Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfcom3 Structured version   Visualization version   GIF version

Theorem cnfcom3 9169
 Description: Any infinite ordinal 𝐵 is equinumerous to a power of ω. (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c 9171.) (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 4-Jul-2019.)
Hypotheses
Ref Expression
cnfcom.s 𝑆 = dom (ω CNF 𝐴)
cnfcom.a (𝜑𝐴 ∈ On)
cnfcom.b (𝜑𝐵 ∈ (ω ↑o 𝐴))
cnfcom.f 𝐹 = ((ω CNF 𝐴)‘𝐵)
cnfcom.g 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
cnfcom.t 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
cnfcom.k 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
cnfcom.w 𝑊 = (𝐺 dom 𝐺)
cnfcom3.1 (𝜑 → ω ⊆ 𝐵)
cnfcom.x 𝑋 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹𝑊) ·o 𝑣) +o 𝑢))
cnfcom.y 𝑌 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))
cnfcom.n 𝑁 = ((𝑋𝑌) ∘ (𝑇‘dom 𝐺))
Assertion
Ref Expression
cnfcom3 (𝜑𝑁:𝐵1-1-onto→(ω ↑o 𝑊))
Distinct variable groups:   𝑥,𝑘,𝑧,𝐴   𝑢,𝑘,𝑣,𝑥,𝑧   𝑥,𝑀   𝜑,𝑢,𝑣   𝑓,𝑘,𝑢,𝑣,𝑥,𝑧,𝐹   𝑢,𝐾,𝑣   𝑢,𝑇,𝑣,𝑧   𝑢,𝑊,𝑣,𝑥   𝑓,𝐺,𝑘,𝑢,𝑣,𝑥,𝑧   𝑓,𝐻,𝑢,𝑣,𝑥   𝑆,𝑘,𝑧   𝜑,𝑘,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑣,𝑢,𝑓)   𝐵(𝑥,𝑧,𝑣,𝑢,𝑓,𝑘)   𝑆(𝑥,𝑣,𝑢,𝑓)   𝑇(𝑥,𝑓,𝑘)   𝐻(𝑧,𝑘)   𝐾(𝑥,𝑧,𝑓,𝑘)   𝑀(𝑧,𝑣,𝑢,𝑓,𝑘)   𝑁(𝑥,𝑧,𝑣,𝑢,𝑓,𝑘)   𝑊(𝑧,𝑓,𝑘)   𝑋(𝑥,𝑧,𝑣,𝑢,𝑓,𝑘)   𝑌(𝑥,𝑧,𝑣,𝑢,𝑓,𝑘)

Proof of Theorem cnfcom3
StepHypRef Expression
1 omelon 9111 . . . . . 6 ω ∈ On
2 cnfcom.a . . . . . . 7 (𝜑𝐴 ∈ On)
3 suppssdm 7845 . . . . . . . . 9 (𝐹 supp ∅) ⊆ dom 𝐹
4 cnfcom.f . . . . . . . . . . . 12 𝐹 = ((ω CNF 𝐴)‘𝐵)
5 cnfcom.s . . . . . . . . . . . . . . 15 𝑆 = dom (ω CNF 𝐴)
61a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → ω ∈ On)
75, 6, 2cantnff1o 9161 . . . . . . . . . . . . . 14 (𝜑 → (ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴))
8 f1ocnv 6629 . . . . . . . . . . . . . 14 ((ω CNF 𝐴):𝑆1-1-onto→(ω ↑o 𝐴) → (ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆)
9 f1of 6617 . . . . . . . . . . . . . 14 ((ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto𝑆(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
107, 8, 93syl 18 . . . . . . . . . . . . 13 (𝜑(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
11 cnfcom.b . . . . . . . . . . . . 13 (𝜑𝐵 ∈ (ω ↑o 𝐴))
1210, 11ffvelrnd 6854 . . . . . . . . . . . 12 (𝜑 → ((ω CNF 𝐴)‘𝐵) ∈ 𝑆)
134, 12eqeltrid 2919 . . . . . . . . . . 11 (𝜑𝐹𝑆)
145, 6, 2cantnfs 9131 . . . . . . . . . . 11 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
1513, 14mpbid 234 . . . . . . . . . 10 (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
1615simpld 497 . . . . . . . . 9 (𝜑𝐹:𝐴⟶ω)
173, 16fssdm 6532 . . . . . . . 8 (𝜑 → (𝐹 supp ∅) ⊆ 𝐴)
18 cnfcom.w . . . . . . . . 9 𝑊 = (𝐺 dom 𝐺)
19 ovex 7191 . . . . . . . . . . . . . . 15 (𝐹 supp ∅) ∈ V
20 cnfcom.g . . . . . . . . . . . . . . . 16 𝐺 = OrdIso( E , (𝐹 supp ∅))
2120oion 9002 . . . . . . . . . . . . . . 15 ((𝐹 supp ∅) ∈ V → dom 𝐺 ∈ On)
2219, 21ax-mp 5 . . . . . . . . . . . . . 14 dom 𝐺 ∈ On
2322elexi 3515 . . . . . . . . . . . . 13 dom 𝐺 ∈ V
2423uniex 7469 . . . . . . . . . . . 12 dom 𝐺 ∈ V
2524sucid 6272 . . . . . . . . . . 11 dom 𝐺 ∈ suc dom 𝐺
26 cnfcom.h . . . . . . . . . . . 12 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
27 cnfcom.t . . . . . . . . . . . 12 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
28 cnfcom.m . . . . . . . . . . . 12 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
29 cnfcom.k . . . . . . . . . . . 12 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
30 cnfcom3.1 . . . . . . . . . . . . 13 (𝜑 → ω ⊆ 𝐵)
31 peano1 7603 . . . . . . . . . . . . . 14 ∅ ∈ ω
3231a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∅ ∈ ω)
3330, 32sseldd 3970 . . . . . . . . . . . 12 (𝜑 → ∅ ∈ 𝐵)
345, 2, 11, 4, 20, 26, 27, 28, 29, 18, 33cnfcom2lem 9166 . . . . . . . . . . 11 (𝜑 → dom 𝐺 = suc dom 𝐺)
3525, 34eleqtrrid 2922 . . . . . . . . . 10 (𝜑 dom 𝐺 ∈ dom 𝐺)
3620oif 8996 . . . . . . . . . . 11 𝐺:dom 𝐺⟶(𝐹 supp ∅)
3736ffvelrni 6852 . . . . . . . . . 10 ( dom 𝐺 ∈ dom 𝐺 → (𝐺 dom 𝐺) ∈ (𝐹 supp ∅))
3835, 37syl 17 . . . . . . . . 9 (𝜑 → (𝐺 dom 𝐺) ∈ (𝐹 supp ∅))
3918, 38eqeltrid 2919 . . . . . . . 8 (𝜑𝑊 ∈ (𝐹 supp ∅))
4017, 39sseldd 3970 . . . . . . 7 (𝜑𝑊𝐴)
41 onelon 6218 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑊𝐴) → 𝑊 ∈ On)
422, 40, 41syl2anc 586 . . . . . 6 (𝜑𝑊 ∈ On)
43 oecl 8164 . . . . . 6 ((ω ∈ On ∧ 𝑊 ∈ On) → (ω ↑o 𝑊) ∈ On)
441, 42, 43sylancr 589 . . . . 5 (𝜑 → (ω ↑o 𝑊) ∈ On)
4516, 40ffvelrnd 6854 . . . . . 6 (𝜑 → (𝐹𝑊) ∈ ω)
46 nnon 7588 . . . . . 6 ((𝐹𝑊) ∈ ω → (𝐹𝑊) ∈ On)
4745, 46syl 17 . . . . 5 (𝜑 → (𝐹𝑊) ∈ On)
48 cnfcom.y . . . . . 6 𝑌 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))
49 cnfcom.x . . . . . 6 𝑋 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹𝑊) ·o 𝑣) +o 𝑢))
5048, 49omf1o 8622 . . . . 5 (((ω ↑o 𝑊) ∈ On ∧ (𝐹𝑊) ∈ On) → (𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→((𝐹𝑊) ·o (ω ↑o 𝑊)))
5144, 47, 50syl2anc 586 . . . 4 (𝜑 → (𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→((𝐹𝑊) ·o (ω ↑o 𝑊)))
5216ffnd 6517 . . . . . . . . . 10 (𝜑𝐹 Fn 𝐴)
53 0ex 5213 . . . . . . . . . . 11 ∅ ∈ V
5453a1i 11 . . . . . . . . . 10 (𝜑 → ∅ ∈ V)
55 elsuppfn 7840 . . . . . . . . . 10 ((𝐹 Fn 𝐴𝐴 ∈ On ∧ ∅ ∈ V) → (𝑊 ∈ (𝐹 supp ∅) ↔ (𝑊𝐴 ∧ (𝐹𝑊) ≠ ∅)))
5652, 2, 54, 55syl3anc 1367 . . . . . . . . 9 (𝜑 → (𝑊 ∈ (𝐹 supp ∅) ↔ (𝑊𝐴 ∧ (𝐹𝑊) ≠ ∅)))
57 simpr 487 . . . . . . . . 9 ((𝑊𝐴 ∧ (𝐹𝑊) ≠ ∅) → (𝐹𝑊) ≠ ∅)
5856, 57syl6bi 255 . . . . . . . 8 (𝜑 → (𝑊 ∈ (𝐹 supp ∅) → (𝐹𝑊) ≠ ∅))
5939, 58mpd 15 . . . . . . 7 (𝜑 → (𝐹𝑊) ≠ ∅)
60 on0eln0 6248 . . . . . . . 8 ((𝐹𝑊) ∈ On → (∅ ∈ (𝐹𝑊) ↔ (𝐹𝑊) ≠ ∅))
6145, 46, 603syl 18 . . . . . . 7 (𝜑 → (∅ ∈ (𝐹𝑊) ↔ (𝐹𝑊) ≠ ∅))
6259, 61mpbird 259 . . . . . 6 (𝜑 → ∅ ∈ (𝐹𝑊))
635, 2, 11, 4, 20, 26, 27, 28, 29, 18, 30cnfcom3lem 9168 . . . . . . 7 (𝜑𝑊 ∈ (On ∖ 1o))
64 ondif1 8128 . . . . . . . 8 (𝑊 ∈ (On ∖ 1o) ↔ (𝑊 ∈ On ∧ ∅ ∈ 𝑊))
6564simprbi 499 . . . . . . 7 (𝑊 ∈ (On ∖ 1o) → ∅ ∈ 𝑊)
6663, 65syl 17 . . . . . 6 (𝜑 → ∅ ∈ 𝑊)
67 omabs 8276 . . . . . 6 ((((𝐹𝑊) ∈ ω ∧ ∅ ∈ (𝐹𝑊)) ∧ (𝑊 ∈ On ∧ ∅ ∈ 𝑊)) → ((𝐹𝑊) ·o (ω ↑o 𝑊)) = (ω ↑o 𝑊))
6845, 62, 42, 66, 67syl22anc 836 . . . . 5 (𝜑 → ((𝐹𝑊) ·o (ω ↑o 𝑊)) = (ω ↑o 𝑊))
6968f1oeq3d 6614 . . . 4 (𝜑 → ((𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→((𝐹𝑊) ·o (ω ↑o 𝑊)) ↔ (𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→(ω ↑o 𝑊)))
7051, 69mpbid 234 . . 3 (𝜑 → (𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→(ω ↑o 𝑊))
715, 2, 11, 4, 20, 26, 27, 28, 29, 18, 33cnfcom2 9167 . . 3 (𝜑 → (𝑇‘dom 𝐺):𝐵1-1-onto→((ω ↑o 𝑊) ·o (𝐹𝑊)))
72 f1oco 6639 . . 3 (((𝑋𝑌):((ω ↑o 𝑊) ·o (𝐹𝑊))–1-1-onto→(ω ↑o 𝑊) ∧ (𝑇‘dom 𝐺):𝐵1-1-onto→((ω ↑o 𝑊) ·o (𝐹𝑊))) → ((𝑋𝑌) ∘ (𝑇‘dom 𝐺)):𝐵1-1-onto→(ω ↑o 𝑊))
7370, 71, 72syl2anc 586 . 2 (𝜑 → ((𝑋𝑌) ∘ (𝑇‘dom 𝐺)):𝐵1-1-onto→(ω ↑o 𝑊))
74 cnfcom.n . . 3 𝑁 = ((𝑋𝑌) ∘ (𝑇‘dom 𝐺))
75 f1oeq1 6606 . . 3 (𝑁 = ((𝑋𝑌) ∘ (𝑇‘dom 𝐺)) → (𝑁:𝐵1-1-onto→(ω ↑o 𝑊) ↔ ((𝑋𝑌) ∘ (𝑇‘dom 𝐺)):𝐵1-1-onto→(ω ↑o 𝑊)))
7674, 75ax-mp 5 . 2 (𝑁:𝐵1-1-onto→(ω ↑o 𝑊) ↔ ((𝑋𝑌) ∘ (𝑇‘dom 𝐺)):𝐵1-1-onto→(ω ↑o 𝑊))
7773, 76sylibr 236 1 (𝜑𝑁:𝐵1-1-onto→(ω ↑o 𝑊))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ≠ wne 3018  Vcvv 3496   ∖ cdif 3935   ∪ cun 3936   ⊆ wss 3938  ∅c0 4293  ∪ cuni 4840   class class class wbr 5068   ↦ cmpt 5148   E cep 5466  ◡ccnv 5556  dom cdm 5557   ∘ ccom 5561  Oncon0 6193  suc csuc 6195   Fn wfn 6352  ⟶wf 6353  –1-1-onto→wf1o 6356  ‘cfv 6357  (class class class)co 7158   ∈ cmpo 7160  ωcom 7582   supp csupp 7832  seqωcseqom 8085  1oc1o 8097   +o coa 8101   ·o comu 8102   ↑o coe 8103   finSupp cfsupp 8835  OrdIsocoi 8975   CNF ccnf 9126 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-inf2 9106 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-seqom 8086  df-1o 8104  df-2o 8105  df-oadd 8108  df-omul 8109  df-oexp 8110  df-er 8291  df-map 8410  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-oi 8976  df-cnf 9127 This theorem is referenced by:  cnfcom3clem  9170
 Copyright terms: Public domain W3C validator