List of theorems referencing the symbol nelt
(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)))))
(182) Theorem 143: [Cardinality minimum theorem] S notin #S
(190) Theorem 151: [Cardinality theorem] Card(#S) & Ord(#S) & (EXISTS f in OM | one_1_map(f) & (range(f) = S) & (domain(f) = #S))
(191) Theorem 152: [One-one maps are cardinality preserving] one_1_map(F) •imp (#range(F) = #domain(F))
(192) Theorem 153: [Equicardinality is equivalent to one-one correspondence] (EXISTS F in OM | (one_1_map(F) & (range(F) = S) & (domain(F) = T))) •eq (#S = #T)
(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))
(194) Theorem 155: [Associative Law for Cardinals] #((A •PROD B) •PROD C) = #(A •PROD (B •PROD C))
(195) Theorem 156: [Commutative Law for Cardinals] #(A •PROD B) = #(B •PROD A)
(196) Theorem 157: [Sets of cardinality 0 must be null] (#S = 0) •eq (S = 0)
(197) Theorem 158: [Non-null sets have cardinality greater than 0] (0 in #S) •eq (S /= 0)
(198) Theorem 159: [A cardinal is its own cardinality] Card(S) •eq (S = #S)
(199) Theorem 160: [Uniqueness of Cardinality] (Card(C) & (EXISTS f in OM | (one_1_map(f) & (range(f) = S) & domain(f) = C))) •imp (C = #S)
(200) Theorem 161: [The cardinality operator is idempotent] #S = ##S
(201) Theorem 162: [All cardinals are comparable] #S in #T or #S = #T or #T in #S
(202) Theorem 163: [Cardinal comparison is transitive] ((#S in #T) & (#T in #R)) •imp (#S in #R)
(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)
(204) Theorem 165: [Subset cardinality theorem] (T •incin S) •imp (#T •incin #S)
(205) Theorem 166: [Single-valued mapping cannot increase cardinality] Svm(F) •imp (#range(F) •incin #domain(F))
(206) Theorem 167: [The cardinality of a map is no smaller than the cardinality of its domain] #domain(F) •incin #F
(207) Theorem 168: [The cardinality of a map is no smaller than the cardinality of its range] #range(F) •incin #F
(208) Theorem 169: [The cardinality of a single-valued map equals the cardinality of its domain] Svm(F) •imp (#domain(F) = #F)
(209) Theorem 170: [Cardinality of restriction maps] (Svm(F) & (domain(F) incs A)) •imp (#(F •ON A) = #A)
(210) Theorem fcn_symbol1: [Cardinality of mapformers and range formers] (#{[xx,f(xx)]: xx in s} = #s) & (#{f(xx): xx in s} •incin #s)
(211) Theorem 171: [Condition for existence of a single-valued map between two sets] (#S incs #T) •eq (T = 0 or (EXISTS f in OM | Svm(f) & (domain(f) = S) & (range(f) = T)))
(229) Theorem 188: [A set is finite if and only if its cardinality is finite] Finite(S) •eq Finite(#S)
(230) Theorem 189: [Proper subsets of a finite set have fewer elements] (Finite(S) & (T •incin S) & (T /= S)) •imp (#T in #S)
(240) Theorem 199: [Infinite cardinality theorem] not Finite(#s_inf)
(245) Theorem setformer_meet_join.4: [Setformer cardinality inclusion, two-variable case] #{[u,v]: u in s, v in t | R(u,v)} incs #{h(u,v): u in s, v in t | R(u,v)}
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(256) Theorem 210: [First Disjoint sum lemma] ((N * M = 0) & (K * J = 0) & (#N = #K) & (#M = #J)) •imp (#(N + M) = #(K + J))
(257) Theorem 211: [Cardinality of Cartesian product by a singleton] (#{[x,A]: x in M} = #M)
(259) Theorem 213: [Disjoint sum lemma] (N * M = 0) •imp (N •PLUS M = #(N + M))
(260) Theorem 214: [Arithmetic addition lemma] N •PLUS M = #N •PLUS #M
(261) Theorem 215: [Second Disjoint sum lemma] (N * M = 0) •imp (#N •PLUS #M = #(N + M))
(262) Theorem 216: [Cardinality of Cartesian product by a singleton, 2] #({C} •PROD N) = #N
(263) Theorem 217: [Cardinality of Cartesian product by a singleton, 3] #(N •PROD {C}) = #N
(264) Theorem 218: [Cardinality of a Cartesian product union] (A /= B) •imp (#N •PLUS #M = #((N •PROD {A}) + (M •PROD {B})))
(265) Theorem 219: [Arithmetic addition lemma 2] N •PLUS M = N •PLUS #M
(266) Theorem 220: [Arithmetic addition lemma 3] N •PLUS M = #N •PLUS M
(267) Theorem 221: [Arithmetic associativity lemma] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp (((N •PLUS M) •PLUS K) = #((N + M) + K))
(268) Theorem 222: [Arithmetic associativity lemma 2] ((N * M = 0) & (N * K = 0) & (M * K = 0)) •imp ((N •PLUS (M •PLUS K)) = #(N + (M + K)))
(269) Theorem 223: [Arithmetic multiplication lemma] (N •TIMES M) = (#N •TIMES #M)
(270) Theorem 224: [Arithmetic multiplication lemma 2] N •TIMES M = N •TIMES #M
(271) Theorem 225: [Arithmetic multiplication lemma 3] #(N •PROD M) = #(#N •PROD #M)
(272) Theorem 226: [Arithmetic multiplication lemma 4] #(N •PROD M) = #(N •PROD #M)
(273) Theorem 227: [Arithmetic multiplication lemma 5] #(N •PROD M) = #(#N •PROD M)
(274) Theorem 228: [Strict monotonicity of finite cardinality] (Finite(N) & (M •incin N) & (M /= N)) •imp (#M in #N)
(286) Theorem 239: [0 is a right additive identity] (#N •PLUS 0) = #N
(287) Theorem 240: [1 is a left multiplicative identity] (1 •TIMES N) = #N
(288) Theorem 241: [1 is a right multiplicative identity] (N •TIMES 1) = #N
(289) Theorem 242: [Monotonicity of multiplication] (M /= 0) •imp (#(N •PROD M) incs #N)
(290) Theorem 243: [Distributivity lemma] (A /= B) •imp (N •PLUS M = #((N •PROD {A}) + (M •PROD {B})))
(304) Theorem 257: [Cantor's Theorem] #N in #pow(N)
(306) Theorem 259: [0 is right identity for arithmetic subtraction] N •MINUS 0 = #N
(307) Theorem 260: [Disjoint additivity lemma] ((N * M = 0) & (N2 * M2 = 0) & (#N = #N2) & (#M = #M2)) •imp (#(N + M) = #(N2 + M2))
(309) Theorem 262: [Subtraction lemma] (M •incin N) •imp (#N = #M •PLUS (N •MINUS M))
(310) Theorem 263: [Subtraction in the non-negative case] (M •incin N) •imp (#N = (N •MINUS M) •PLUS M)
(311) Theorem 264: [Subtraction lemma 2] (#M in #N or #M = #N) •imp (#N = #M •PLUS (#N •MINUS #M))
(319) Theorem 272: [Only the nullset has cardinality zero] (#N = 0) •imp (N = 0)
(339) Theorem 292: [Singletons have one element] #{S} = {0}
(343) Theorem 296: [Cardinality of set difference] (Finite(N) & (N incs M)) •imp (#(N - M) = #(#N - #M))
(345) Theorem 298: [Addition reverses subtraction] (N incs M) •imp (#N = #M •PLUS #(N - M))
(348) Theorem 301: [The successor integer as a sum] (N •PLUS 1) = #next(N)
(361) Theorem 314: (({X,Y} •incin next(Za)) & (#X in next(Y))) •imp (((X = Y) & (Y = Za)) or (X in (next(Y) * Za)))
(368) Theorem 317: ((N in Za) & (S •incin N) & (#S = N)) •imp (S = N)
(370) Theorem 319: [Other properties of finite sequences] (F in Fin_seqs(S)) •imp ((domain(F) = #domain(F)) & (domain(F) = #F) & (#F in Za) & Finite(F))
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(380) Theorem 329: ((F in Fin_seqs(S)) & (M in Za)) •imp (((F •ON M) in Fin_seqs(S)) & (shifted_seq(F,M) in Fin_seqs(S)) & (domain(shifted_seq(F,M)) = (#F •MINUS M)))
(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)
(431) Theorem 338: ['One-more' lemma] (not Finite(S)) •imp (#S = #(S + {C}))
(432) Theorem 339: ['Few-more' lemma] ((not Finite(S)) & Finite(T)) •imp (#S = #(S + T))
(433) Theorem 340: [Any infinite cardinal is a limit ordinal] ((not Finite(S)) & (X in #S)) •imp (X + {X} in #S)
(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)
(435) Theorem 342: [The cardinality of a non-null Cartesian product is at least the cardinality of its first factor] (T /= 0) •imp (#S •incin #(S •PROD T))
(438) Theorem 345: [Cardinal Doubling Theorem] (not Finite(S)) •imp (#(S •PROD {0,1}) = #S)
(439) Theorem 346: [The sum of two infinite quantities is their maximum] (not Finite(S)) •imp ((S •PLUS T) = #S + #T)
(440) Theorem 347: [The cardinality of the union of two infinite quantities is the cardinality of the larger] (not Finite(S)) •imp (#(S + T) = #S + #T)
(441) Theorem 348: [Cardinal Square Theorem] (not Finite(S)) •imp (#(S •PROD S) = #S)
(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})))