List of theorems referencing the symbol UN
(31) Theorem 20: [Ultimate members of the basic infinite set] (X in s_inf) •imp (membs_x(S,{X}) = membs_x(S,X) + Un(membs_x(S,X)))
(136) Theorem 103: [Union set of a doubleton] Un({X,Y}) = (X + Y)
(137) Theorem 104: [Union set of a singleton] Un({X}) = X
(138) Theorem 105: [Recursive relationship for the union set] (Un(0) = 0) & ((M /= 0) •imp (Un(M) = (arb(M) + Un(M - {arb(M)}))))
(139) Theorem unionset_commuter1: [Set separation and unionset formation commute] {e(x): x in Un(s)} = Un({{e(x): x in f}: f in s})
(140) Theorem unionset_commuter2: [Set formation and set enumeration commute] {e(x): x in s} = Un({{e(x)}: x in s})
(145) Theorem 106: [Map inversion and unionset formation commute] inv(Un(S)) = Un({inv(f): f in S})
(146) Theorem 107: [Range formation and unionset formation commute] range(Un(S)) = Un({range(f): f in S})
(147) Theorem 108: [Domain formation and unionset formation commute] domain(Un(S)) = Un({domain(f): f in S})
(278) Theorem 231: [The union of finitely many finite sets is finite] ((FORALL x in S | Finite(x)) & Finite(S)) •imp Finite(Un(S))
(312) Theorem 265: [Union set as an upper bound] (FORALL x in S | x •incin Un(S)) & ((FORALL x in S | x •incin T) •imp (Un(S) •incin T))
(313) Theorem 266: [Monotonicity of the union-set operator] (S •incin T) •imp (Un(S) •incin Un(T))
(314) Theorem 267: [The union of a set of ordinals is an ordinal] (FORALL x in S | Ord(x)) •imp Ord(Un(S))
(350) Theorem 303: [The union set of a finite collection of integers is an integer] ((M •incin Za) & Finite(M)) •imp (((M /= 0) •imp (Un(M) in M)) & (Un(M) in Za))
(351) Theorem 304: [The union set of a set of integers is the least upper bound of its elements] (M in Za) •imp (((Un(M) in Za) & (Un(M) •incin M)) & ((M /= 0) •imp (Un(M) in M)))
(352) Theorem 305: [Every nonzero integer has a predecessor] ((M in Za) & (M /= 0)) •imp (M = (Un(M) •PLUS 1))
(503) Theorem wellfounded_recursive_fcn.4: (FORALL x, t | (x in s) •imp (rk_thryvar(x,t) = Un({next(rk_thryvar(y,t)): y in s | arg1_bef_arg2(y,x) & ([y,x] in t)})))
(546) Theorem 397: [Zorn's lemma for union-closed collections] (FORALL x •incin T | ((FORALL u in x,v in x | (u incs v or v incs u)) •imp (Un(x) in T))) •imp (FORALL u in T | (EXISTS y in T | (y incs u) & (FORALL x in T | not ((x incs y) & (x /= y)))))
(547) Theorem 398: ((FORALL t in TP | Filter(t,S)) & (FORALL u in TP, v in TP | (u incs v or v incs u))) •imp Filter(Un(TP),S)
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))