List of theorems referencing the symbol ORD

(22) Theorem 12: [Members of ordinals are ordinals] (Ord(S) & (T in S)) •imp Ord(T)
(23) Theorem 13: [Ordinal membership implies inclusion] (Ord(S) & (T in S)) •imp (T •incin S)
(24) Theorem ord_ind1: [Transfinite induction principle] Ord(t_thryvar) & P(t_thryvar) & (t_thryvar •incin o) & (FORALL x in t_thryvar | not P(x))
(28) Theorem 17: [An ordinal is its own set of ultimate members] (Ord(S)) •imp (Ult_membs(S) = S)
(30) Theorem 19: [Ultimate members of an ordinal singleton] Ord(S) •imp (Ult_membs({S}) = S + {S})
(49) Theorem 27: [Ordinal comparison lemma] (Ord(S) & Ord(T) & (T •incin S)) •imp ((T = S) or (T = arb(S - T)))
(50) Theorem 28: [Ordinal intersection] (Ord(S) & Ord(T)) •imp Ord(S * T)
(51) Theorem 29: [Second order comparison lemma] (Ord(S) & Ord(T)) •imp ((S •incin T) or (T •incin S))
(52) Theorem 30: [Ordinal maximum and minimum] (Ord(S) & Ord(T)) •imp (Ord(S + T) & Ord(S * T))
(53) Theorem 31: [Ordinal membership comparison] (Ord(S) & Ord(T)) •imp ((S in T) or (T in S) or (S = T))
(54) Theorem 32: [Successor ordinal] Ord(S) •imp Ord(next(S))
(55) Theorem 33: [Successor ordinal 2] Ord(S) •imp Ord(S + {S})
(56) Theorem 34: [Third ordinal comparison lemma] (Ord(S) & Ord(T)) •imp ((T •incin S) •eq ((T in S) or (T = S)))
(57) Theorem 35: [Ordinal membership and comparison] (Ord(S) & Ord(T)) •imp ((T notin S) •eq (S •incin T))
(58) Theorem 36: [Membership in the successor of an ordinal s] Ord(S) •imp ((T in next(S)) •eq ((T •incin S) & Ord(T)))
(59) Theorem 37: [Membership of s in an ordinal t implies inclusion of next(s) in t] (Ord(T) & (S in T)) •imp (next(S) •incin T)
(62) Theorem 40: [The class of ordinals is not a set] not (FORALL x | ((x in OS) •eq Ord(x)))
(63) Theorem 41: [Enumerability principle] ((Ord(X) & S in {enum(y,S): y in X})) •imp (S •incin {enum(y,S): y in X})
(66) Theorem 44: [The enumeration of a set is 1-1] (Ord(X) & Ord(W) & (X /= W)) •imp (S in {enum(u,S): u in X} or S in {enum(u,S): u in W} or enum(X,S) /= enum(W,S))
(67) Theorem 45: [Enumeration lemma] (EXISTS x | (Ord(x) & (S in {enum(y,S): y in x})))
(68) Theorem 46: [Main enumeration theorem] (EXISTS x | Ord(x) & (S = {enum(y,S): y in x}) & (FORALL y in x, z0 in x | ((y /= z0) •imp (enum(y,S) /= enum(z0,S)))))
(68+) Theorem 47: [Enumeration single-valuedness principle] (FORALL s | (Ord(enum_Ord(s)) & (s = {enum(y,s): y in enum_Ord(s)}) & (FORALL y in enum_Ord(s), z0 in enum_Ord(s) | ((y /= z0) •imp (enum(y,s) /= enum(z0,s))))))
(180) Theorem 141: [Enumeration of an ordinal] (Ord(S) & X in S) •imp (enum(X,S) = X)
(181) Theorem 142: [Cardinality lemma] Ord(#S) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & (domain(f) = #S))) & (not((EXISTS o in #S | (EXISTS g in OM | one_1_map(g) & (range(g) = S) & (domain(g) = o)))))
(183) Theorem 144: ['arb' is monotone decreasing for non-empty sets of ordinals] (Ord(R) & (R incs S) & (S incs T)) •imp (arb(S) in arb(T) or arb(S) = arb(T) or T = 0)
(184) Theorem 145: [Axiom of choice variant] ((S /= 0) & (FORALL x in S | Ord(x))) •imp (FORALL x in S | x incs arb(S))
(185) Theorem 146: [Lemma for ordinal enumeration] (Ord(S) & (T •incin S) & (X in S) & (Y in X)) •imp (enum(Y,T) in enum(X,T) or enum(X,T) incs T)
(186) Theorem 147: [Subsets of an ordinal enumerate at least as rapidly as the ordinal] (Ord(S) & (T •incin S) & (X in S)) •imp (enum(X,T) incs X or enum(X,T) incs T)
(187) Theorem 148: [Subset enumeration lemma] (Ord(S) & (T •incin S)) •imp ({enum(x,T): x in S} incs T)
(188) Theorem 149: [Second subset enumeration lemma] (Ord(S) & (T •incin S)) •imp (EXISTS x •incin S | (Ord(x) & (T = {enum(y,T): y in x}) & (FORALL y in x, z in x | ((y /= z) •imp (enum(y,T) /= enum(z,T))))))
(189) Theorem 150: [Enumerability lemma] (Ord(S) & (T •incin S)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (domain(f) •incin S) & (range(f) = T))
(190) Theorem 151: [Cardinality theorem] Card(#S) & Ord(#S) & (EXISTS f in OM | one_1_map(f) & (range(f) = S) & (domain(f) = #S))
(193) Theorem 154: [The enumerating ordinal of a set has the same cardinality as the set] (EXISTS o | Ord(o) & (S = {enum(x,S): x in o}) & (#o = #S))
(203) Theorem 164: [Subsets of an ordinal have a cardinality that is no larger than the ordinal] (Ord(S) & (T •incin S)) •imp (#T •incin S)
(223) Theorem 183: [0 is a finite cardinal] Ord(0) & Finite(0) & Card(0)
(232) Theorem 191: [Members of a finite ordinal are finite] (Ord(S) & Finite(S) & (T in S)) •imp Finite(T)
(233) Theorem 192: [Any infinite ordinal is larger than any finite ordinal] (Ord(S) & Ord(T) & (not Finite(S)) & Finite(T)) •imp (T in S)
(241) Theorem 200: [All finite ordinals are cardinals] (Ord(X) & Finite(X)) •imp Card(X)
(247) Theorem 201: [The set of integers is an infinite ordinal consisting of all finite ordinals] Ord(Za) & (not Finite(Za)) & ((Card(X) & Finite(X)) •eq (X in Za))
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(252) Theorem 206: [The first few integers are all cardinals] Ord(0) & (0 in Za) & (1 in Za) & (2 in Za) & (3 in Za) & Card(0) & Card(1) & Card(2) & Card(3)
(308) Theorem 261: [Excess subtraction lemma] (Ord(Y) & (X in Y)) •imp ((X •MINUS Y) = 0)
(314) Theorem 267: [The union of a set of ordinals is an ordinal] (FORALL x in S | Ord(x)) •imp Ord(Un(S))
(363) Theorem unsigned_integer_bynd.1: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (Za incs bynd_thryvar) & Ord(bynd_thryvar) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar))) & (not Finite(Za - bynd_thryvar))
(365) Theorem 315: [Ordinal member maximum and minimum] (Ord(U) & (S in U) & (T in U)) •imp ((S + T in U) & (S * T in U))
(405) Theorem well_founded_set.5: [Ordinal enumeration is monotone on ordinals] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(407) Theorem well_founded_set.7: [Well-ordering is initially 1-1] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s) & (U /= V)) •imp (ordenm_thryvar(U) /= ordenm_thryvar(V))
(408) Theorem well_founded_set.8: (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o})))
(409) Theorem well_founded_set.9: (ord_thryvar in next(#pow(s))) & Ord(ord_thryvar) & (s = {ordenm_thryvar(x): x in ord_thryvar}) & (FORALL x in ord_thryvar | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in ord_thryvar})
(412) Theorem well_ordered_set.100: (FORALL x,y | ((x in s) & (y in s)) •imp ((not (arg1_bef_arg2(x,y) & arg1_bef_arg2(y,x))) & (not arg1_bef_arg2(x,x)))) & (FORALL x | (not(s •incin {ordenm_thryvar(y): y in x})) •imp ((ordenm_thryvar(x) in (s - {ordenm_thryvar(y): y in x})) & (FORALL y in (s - {ordenm_thryvar(y): y in x}) | not(arg1_bef_arg2(y,ordenm_thryvar(x)))))) & (FORALL x | (s •incin {ordenm_thryvar(y): y in x}) •eq (ordenm_thryvar(x) = s)) & (FORALL x | (ordenm_thryvar(x) /= s) •imp (ordenm_thryvar(x) in s)) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & arg1_bef_arg2(ordenm_thryvar(u),ordenm_thryvar(v))) •imp (u in v)) & (FORALL v | {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(v))} •incin {ordenm_thryvar(x): x in v}) & (FORALL u, v | (Ord(u) & Ord(v) & (ordenm_thryvar(u) /= s) & (ordenm_thryvar(v) /= s) & (u /= v)) •imp (ordenm_thryvar(u) /= ordenm_thryvar(v))) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o}))) & (FORALL x | ordenm_thryvar(x) = Minrel_thryvar(s - {ordenm_thryvar(y): y in x})) & (FORALL t | Minrel_thryvar(t) = if (t •incin s) & (t /= 0) then arb({m: m in t | (FORALL y in t | (not arg1_bef_arg2(y,m)))}) else s end if)
(416) Theorem well_ordered_set.5a: (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V))) •imp (U in V)
(418) Theorem well_ordered_set.7: ((Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s) & (U /= V)) •imp (ordenm_thryvar(U) /= ordenm_thryvar(V)))
(419) Theorem well_ordered_set.8: (EXISTS o | (Ord(o) & (s = {ordenm_thryvar(x): x in o}) & (FORALL x in o | (ordenm_thryvar(x) /= s)) & one_1_map({[x,ordenm_thryvar(x)]: x in o})))
(422) Theorem well_ordered_set.5: [Any well-ordering is isomorphic to an ordinal enumeration] (Ord(U) & Ord(V) & (ordenm_thryvar(U) /= s) & (ordenm_thryvar(V) /= s)) •imp (arg1_bef_arg2(ordenm_thryvar(U),ordenm_thryvar(V)) •eq (U in V))
(423) Theorem well_ordered_set.6: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V})
(424) Theorem well_ordered_set.9: (Ord(V) & (ordenm_thryvar(V) /= s)) •imp ( one_1_map({[x,ordenm_thryvar(x)]: x in V}) & (domain({[x,ordenm_thryvar(x)]: x in V}) = V) & (range({[x,ordenm_thryvar(x)]: x in V}) = {u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))}) & ({u: u in s | arg1_bef_arg2(u,ordenm_thryvar(V))} = {ordenm_thryvar(x): x in V}))
(425) Theorem product_order_1: [The first component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X))
(426) Theorem product_order_2: [The second component of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(cdr(X))
(427) Theorem product_order_3: [The maximum of the components of any member of a Cartesian product of ordinals is an ordinal] (X in o1 •PROD o2) •imp Ord(car(X) + cdr(X))
(434) Theorem 341: [If ordinal S dominates the members of an ordinal T, #S is no less than #T] (Ord(S) & Ord(T) & (not Finite(S)) & (FORALL u in T | #u in #S)) •imp (#T •incin #S)
(436) Theorem 343: (Ord(O1) & Ord(O2)) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f), y in domain(f) | (x in y) •eq (((car(f~[x]) + cdr(f~[x])) in (car(f~[y]) + cdr(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) in car(f~[y]))) or (((car(f~[x]) + cdr(f~[x])) = (car(f~[y]) + cdr(f~[y]))) & (car(f~[x]) = car(f~[y])) & (cdr(f~[x]) in cdr(f~[y]))))))
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(499) Theorem wellfounded_recursive_fcn.100: (FORALL u, v | (Ord(u) & Ord(v) & (orden(u) /= s) & arg1_bef_arg2(orden(u),orden(v))) •imp (u in v)) & (EXISTS o in next(#pow(s)) | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(500) Theorem wellfounded_recursive_fcn.100a: (EXISTS o | (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o})))
(500+) Theorem wellfounded_recursive_fcn.101: (Ord(o) & (s = {orden(x): x in o}) & (FORALL x in o | (orden(x) /= s)) & one_1_map({[x,orden(x)]: x in o}))
(501) Theorem wellfounded_recursive_fcn.1: (V in s) •imp ((index(V) in o) & Ord(index(V)) & (orden(index(V)) = V))