:: On Powers of Cardinals :: by Grzegorz Bancerek :: :: Received August 24, 1992 :: Copyright (c) 1992-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, ORDINAL1, CARD_1, FUNCT_1, ORDINAL2, TARSKI, CARD_3, RELAT_1, FINSET_1, XBOOLE_0, ARYTM_3, WELLORD1, WELLORD2, ORDINAL4, CARD_2, ORDINAL3, ZFMISC_1, FUNCT_2, FUNCOP_1, MCART_1, CARD_5, MEMBERED, NAT_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MEMBERED, RELAT_1, FUNCT_1, FINSET_1, FUNCT_2, WELLORD1, WELLORD2, XTUPLE_0, MCART_1, FUNCOP_1, ORDINAL2, ORDINAL3, CARD_2, CARD_3, ORDINAL4; constructors WELLORD1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, NAT_1, FINSEQ_1, CARD_2, CARD_3, ORDINAL4, RELSET_1, MEMBERED, ORDERS_1, XREAL_0, XTUPLE_0, NUMBERS; registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL2, ORDINAL3, NAT_1, CARD_1, CARD_3, ORDINAL4, MEMBERED, FINSET_1, CARD_2, XTUPLE_0; requirements NUMERALS, BOOLE, SUBSET; begin :: Results of [(30),AXIOMS]. reserve k,n,m for Nat, A,B,C for Ordinal, X for set, x,y,z for object; begin :: Infinity, alephs and cofinality reserve f,g,h,fx for Function, K,M,N for Cardinal, phi,psi for Ordinal-Sequence; theorem :: CARD_5:1 nextcard card X = nextcard X; theorem :: CARD_5:2 y in Union f iff ex x st x in dom f & y in f.x; theorem :: CARD_5:3 aleph A is infinite; theorem :: CARD_5:4 M is infinite implies ex A st M = aleph A; registration let phi; cluster Union phi -> ordinal; end; theorem :: CARD_5:5 X c= A implies ex phi st phi = canonical_isomorphism_of(RelIncl order_type_of RelIncl X, RelIncl X) & phi is increasing & dom phi = order_type_of RelIncl X & rng phi = X; theorem :: CARD_5:6 X c= A implies sup X is_cofinal_with order_type_of RelIncl X; theorem :: CARD_5:7 X c= A implies card X = card order_type_of RelIncl X; theorem :: CARD_5:8 ex B st B c= card A & A is_cofinal_with B; theorem :: CARD_5:9 ex M st M c= card A & A is_cofinal_with M & for B st A is_cofinal_with B holds M c= B; theorem :: CARD_5:10 rng phi = rng psi & phi is increasing & psi is increasing implies phi = psi; theorem :: CARD_5:11 phi is increasing implies phi is one-to-one; theorem :: CARD_5:12 (phi^psi)|(dom phi) = phi; theorem :: CARD_5:13 X <> {} implies card { Y where Y is Subset of X: card Y in M } c= M*` exp(card X,M); theorem :: CARD_5:14 M in exp(2,M); registration cluster infinite for Cardinal; end; registration cluster infinite -> non empty for set; end; definition mode Aleph is infinite Cardinal; let M; func cf M -> Cardinal means :: CARD_5:def 1 M is_cofinal_with it & for N st M is_cofinal_with N holds it c= N; let N; func N-powerfunc_of M -> Cardinal-Function means :: CARD_5:def 2 (for x holds x in dom it iff x in M & x is Cardinal) & for K st K in M holds it.K = exp(K,N); end; registration let A; cluster aleph A -> infinite; end; begin :: Arithmetics of alephs reserve a,b for Aleph; ::$CT theorem :: CARD_5:16 a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a; theorem :: CARD_5:17 a c= M or a in M implies M is Aleph; theorem :: CARD_5:18 a c= M or a in M implies a +` M = M & M +` a = M & a *` M = M & M *` a = M; theorem :: CARD_5:19 a +` a = a & a *` a = a; theorem :: CARD_5:20 M c= exp(M,a); theorem :: CARD_5:21 union a = a; registration let a,M; cluster a +` M -> infinite; end; registration let M,a; cluster M +` a -> infinite; end; registration let a,b; cluster a *` b -> infinite; cluster exp(a,b) -> infinite; end; begin :: Regular alephs definition let IT be Aleph; attr IT is regular means :: CARD_5:def 3 cf IT = IT; end; notation let IT be Aleph; antonym IT is irregular for IT is regular; end; registration let a; cluster nextcard a -> infinite; end; theorem :: CARD_5:22 cf omega = omega; theorem :: CARD_5:23 cf nextcard a = nextcard a; theorem :: CARD_5:24 omega c= cf a; theorem :: CARD_5:25 cf 0 = 0 & cf card (n+1) = 1; theorem :: CARD_5:26 X c= M & card X in cf M implies sup X in M & union X in M; theorem :: CARD_5:27 dom phi = M & rng phi c= N & M in cf N implies sup phi in N & Union phi in N; registration let a; cluster cf a -> infinite; end; theorem :: CARD_5:28 cf a in a implies a is limit_cardinal; theorem :: CARD_5:29 cf a in a implies ex xi being Ordinal-Sequence st dom xi = cf a & rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0 in rng xi; theorem :: CARD_5:30 omega is regular & nextcard a is regular; begin :: Infinite powers reserve a,b for Aleph; theorem :: CARD_5:31 a c= b implies exp(a,b) = exp(2,b); theorem :: CARD_5:32 exp(nextcard a,b) = exp(a,b) *` nextcard a; theorem :: CARD_5:33 Sum (b-powerfunc_of a) c= exp(a,b); theorem :: CARD_5:34 a is limit_cardinal & b in cf a implies exp(a,b) = Sum (b-powerfunc_of a); theorem :: CARD_5:35 cf a c= b & b in a implies exp(a,b) = exp(Sum (b-powerfunc_of a), cf a); reserve O for Ordinal, F for Subset of omega; theorem :: CARD_5:36 for X being finite set st X c= O holds order_type_of RelIncl X = card X; theorem :: CARD_5:37 {x} c= O implies order_type_of RelIncl {x} = 1; theorem :: CARD_5:38 {x} c= O implies canonical_isomorphism_of (RelIncl order_type_of RelIncl {x}, RelIncl {x}) = 0 .--> x; registration let O be Ordinal, X be Subset of O, n be set; cluster canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X) .n -> ordinal; end; registration let X be natural-membered set, n be set; cluster canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X).n -> natural; end; theorem :: CARD_5:39 card F c= order_type_of RelIncl F;