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

Theorem cnfcom3clem 9170
 Description: Lemma for cnfcom3c 9171. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 4-Jul-2019.)
Hypotheses
Ref Expression
cnfcom3c.s 𝑆 = dom (ω CNF 𝐴)
cnfcom3c.f 𝐹 = ((ω CNF 𝐴)‘𝑏)
cnfcom3c.g 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom3c.h 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
cnfcom3c.t 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom3c.m 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
cnfcom3c.k 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
cnfcom3c.w 𝑊 = (𝐺 dom 𝐺)
cnfcom3c.x 𝑋 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹𝑊) ·o 𝑣) +o 𝑢))
cnfcom3c.y 𝑌 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))
cnfcom3c.n 𝑁 = ((𝑋𝑌) ∘ (𝑇‘dom 𝐺))
cnfcom3c.l 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁)
Assertion
Ref Expression
cnfcom3clem (𝐴 ∈ On → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
Distinct variable groups:   𝑔,𝑏,𝑘,𝑢,𝑣,𝑤,𝑥,𝑧,𝐴   𝑢,𝐾,𝑣   𝑔,𝐿,𝑤   𝑥,𝑀   𝑢,𝑇,𝑣,𝑧   𝑓,𝑘,𝑢,𝑣,𝑥,𝑧,𝐹   𝑓,𝐺,𝑘,𝑢,𝑣,𝑥,𝑧   𝑓,𝐻,𝑢,𝑣,𝑥   𝑆,𝑘,𝑧   𝑢,𝑊,𝑣,𝑤,𝑥
Allowed substitution hints:   𝐴(𝑓)   𝑆(𝑥,𝑤,𝑣,𝑢,𝑓,𝑔,𝑏)   𝑇(𝑥,𝑤,𝑓,𝑔,𝑘,𝑏)   𝐹(𝑤,𝑔,𝑏)   𝐺(𝑤,𝑔,𝑏)   𝐻(𝑧,𝑤,𝑔,𝑘,𝑏)   𝐾(𝑥,𝑧,𝑤,𝑓,𝑔,𝑘,𝑏)   𝐿(𝑥,𝑧,𝑣,𝑢,𝑓,𝑘,𝑏)   𝑀(𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,𝑘,𝑏)   𝑁(𝑥,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,𝑘,𝑏)   𝑊(𝑧,𝑓,𝑔,𝑘,𝑏)   𝑋(𝑥,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,𝑘,𝑏)   𝑌(𝑥,𝑧,𝑤,𝑣,𝑢,𝑓,𝑔,𝑘,𝑏)

Proof of Theorem cnfcom3clem
StepHypRef Expression
1 cnfcom3c.s . . . . . 6 𝑆 = dom (ω CNF 𝐴)
2 simp1 1133 . . . . . 6 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ∈ On)
3 omelon 9111 . . . . . . . . 9 ω ∈ On
4 1onn 8266 . . . . . . . . 9 1o ∈ ω
5 ondif2 8128 . . . . . . . . 9 (ω ∈ (On ∖ 2o) ↔ (ω ∈ On ∧ 1o ∈ ω))
63, 4, 5mpbir2an 710 . . . . . . . 8 ω ∈ (On ∖ 2o)
7 oeworde 8220 . . . . . . . 8 ((ω ∈ (On ∖ 2o) ∧ 𝐴 ∈ On) → 𝐴 ⊆ (ω ↑o 𝐴))
86, 2, 7sylancr 590 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝐴 ⊆ (ω ↑o 𝐴))
9 simp2 1134 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑏𝐴)
108, 9sseldd 3918 . . . . . 6 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑏 ∈ (ω ↑o 𝐴))
11 cnfcom3c.f . . . . . 6 𝐹 = ((ω CNF 𝐴)‘𝑏)
12 cnfcom3c.g . . . . . 6 𝐺 = OrdIso( E , (𝐹 supp ∅))
13 cnfcom3c.h . . . . . 6 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
14 cnfcom3c.t . . . . . 6 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
15 cnfcom3c.m . . . . . 6 𝑀 = ((ω ↑o (𝐺𝑘)) ·o (𝐹‘(𝐺𝑘)))
16 cnfcom3c.k . . . . . 6 𝐾 = ((𝑥𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ (𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
17 cnfcom3c.w . . . . . 6 𝑊 = (𝐺 dom 𝐺)
18 simp3 1135 . . . . . 6 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → ω ⊆ 𝑏)
191, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18cnfcom3lem 9168 . . . . 5 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑊 ∈ (On ∖ 1o))
20 cnfcom3c.x . . . . . . 7 𝑋 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((𝐹𝑊) ·o 𝑣) +o 𝑢))
21 cnfcom3c.y . . . . . . 7 𝑌 = (𝑢 ∈ (𝐹𝑊), 𝑣 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑢) +o 𝑣))
22 cnfcom3c.n . . . . . . 7 𝑁 = ((𝑋𝑌) ∘ (𝑇‘dom 𝐺))
231, 2, 10, 11, 12, 13, 14, 15, 16, 17, 18, 20, 21, 22cnfcom3 9169 . . . . . 6 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏1-1-onto→(ω ↑o 𝑊))
24 f1of 6599 . . . . . . . . . 10 (𝑁:𝑏1-1-onto→(ω ↑o 𝑊) → 𝑁:𝑏⟶(ω ↑o 𝑊))
2523, 24syl 17 . . . . . . . . 9 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑁:𝑏⟶(ω ↑o 𝑊))
26 vex 3445 . . . . . . . . 9 𝑏 ∈ V
27 fex 6976 . . . . . . . . 9 ((𝑁:𝑏⟶(ω ↑o 𝑊) ∧ 𝑏 ∈ V) → 𝑁 ∈ V)
2825, 26, 27sylancl 589 . . . . . . . 8 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → 𝑁 ∈ V)
29 cnfcom3c.l . . . . . . . . 9 𝐿 = (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁)
3029fvmpt2 6766 . . . . . . . 8 ((𝑏 ∈ (ω ↑o 𝐴) ∧ 𝑁 ∈ V) → (𝐿𝑏) = 𝑁)
3110, 28, 30syl2anc 587 . . . . . . 7 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → (𝐿𝑏) = 𝑁)
32 f1oeq1 6587 . . . . . . 7 ((𝐿𝑏) = 𝑁 → ((𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑊) ↔ 𝑁:𝑏1-1-onto→(ω ↑o 𝑊)))
3331, 32syl 17 . . . . . 6 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → ((𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑊) ↔ 𝑁:𝑏1-1-onto→(ω ↑o 𝑊)))
3423, 33mpbird 260 . . . . 5 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → (𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑊))
35 oveq2 7153 . . . . . . 7 (𝑤 = 𝑊 → (ω ↑o 𝑤) = (ω ↑o 𝑊))
3635f1oeq3d 6596 . . . . . 6 (𝑤 = 𝑊 → ((𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤) ↔ (𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑊)))
3736rspcev 3572 . . . . 5 ((𝑊 ∈ (On ∖ 1o) ∧ (𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑊)) → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤))
3819, 34, 37syl2anc 587 . . . 4 ((𝐴 ∈ On ∧ 𝑏𝐴 ∧ ω ⊆ 𝑏) → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤))
39383expia 1118 . . 3 ((𝐴 ∈ On ∧ 𝑏𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
4039ralrimiva 3149 . 2 (𝐴 ∈ On → ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
41 ovex 7178 . . . . 5 (ω ↑o 𝐴) ∈ V
4241mptex 6973 . . . 4 (𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁) ∈ V
4329, 42eqeltri 2886 . . 3 𝐿 ∈ V
44 nfmpt1 5132 . . . . . 6 𝑏(𝑏 ∈ (ω ↑o 𝐴) ↦ 𝑁)
4529, 44nfcxfr 2953 . . . . 5 𝑏𝐿
4645nfeq2 2972 . . . 4 𝑏 𝑔 = 𝐿
47 fveq1 6654 . . . . . . 7 (𝑔 = 𝐿 → (𝑔𝑏) = (𝐿𝑏))
48 f1oeq1 6587 . . . . . . 7 ((𝑔𝑏) = (𝐿𝑏) → ((𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤) ↔ (𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
4947, 48syl 17 . . . . . 6 (𝑔 = 𝐿 → ((𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤) ↔ (𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
5049rexbidv 3257 . . . . 5 (𝑔 = 𝐿 → (∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤) ↔ ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
5150imbi2d 344 . . . 4 (𝑔 = 𝐿 → ((ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤)) ↔ (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤))))
5246, 51ralbid 3195 . . 3 (𝑔 = 𝐿 → (∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤)) ↔ ∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤))))
5343, 52spcev 3556 . 2 (∀𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝐿𝑏):𝑏1-1-onto→(ω ↑o 𝑤)) → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
5440, 53syl 17 1 (𝐴 ∈ On → ∃𝑔𝑏𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑔𝑏):𝑏1-1-onto→(ω ↑o 𝑤)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3442   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  ∅c0 4246  ∪ cuni 4804   ↦ cmpt 5114   E cep 5433  ◡ccnv 5522  dom cdm 5523   ∘ ccom 5527  Oncon0 6166  ⟶wf 6328  –1-1-onto→wf1o 6331  ‘cfv 6332  (class class class)co 7145   ∈ cmpo 7147  ωcom 7573   supp csupp 7826  seqωcseqom 8084  1oc1o 8096  2oc2o 8097   +o coa 8100   ·o comu 8101   ↑o coe 8102  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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5158  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454  ax-inf2 9106 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4805  df-int 4843  df-iun 4887  df-br 5035  df-opab 5097  df-mpt 5115  df-tr 5141  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-isom 6341  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7574  df-1st 7684  df-2nd 7685  df-supp 7827  df-wrecs 7948  df-recs 8009  df-rdg 8047  df-seqom 8085  df-1o 8103  df-2o 8104  df-oadd 8107  df-omul 8108  df-oexp 8109  df-er 8290  df-map 8409  df-en 8511  df-dom 8512  df-sdom 8513  df-fin 8514  df-fsupp 8836  df-oi 8976  df-cnf 9127 This theorem is referenced by:  cnfcom3c  9171
 Copyright terms: Public domain W3C validator