Metamath Proof Explorer

Theorem cnfcom3clem

Description: Lemma for cnfcom3c . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 4-Jul-2019)

Ref Expression
Hypotheses 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 cnfcom3clem ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 cnfcom3c.s ⊢ 𝑆 = dom ( ω CNF 𝐴 )
2 cnfcom3c.f ⊢ 𝐹 = ( ◡ ( ω CNF 𝐴 ) ‘ 𝑏 )
3 cnfcom3c.g ⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
4 cnfcom3c.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( 𝑀 +o 𝑧 ) ) , ∅ )
5 cnfcom3c.t ⊢ 𝑇 = seqω ( ( 𝑘 ∈ V , 𝑓 ∈ V ↦ 𝐾 ) , ∅ )
6 cnfcom3c.m ⊢ 𝑀 = ( ( ω ↑o ( 𝐺 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝐺 ‘ 𝑘 ) ) )
7 cnfcom3c.k ⊢ 𝐾 = ( ( 𝑥 ∈ 𝑀 ↦ ( dom 𝑓 +o 𝑥 ) ) ∪ ◡ ( 𝑥 ∈ dom 𝑓 ↦ ( 𝑀 +o 𝑥 ) ) )
8 cnfcom3c.w ⊢ 𝑊 = ( 𝐺 ‘ ∪ dom 𝐺 )
9 cnfcom3c.x ⊢ 𝑋 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( 𝐹 ‘ 𝑊 ) ·o 𝑣 ) +o 𝑢 ) )
10 cnfcom3c.y ⊢ 𝑌 = ( 𝑢 ∈ ( 𝐹 ‘ 𝑊 ) , 𝑣 ∈ ( ω ↑o 𝑊 ) ↦ ( ( ( ω ↑o 𝑊 ) ·o 𝑢 ) +o 𝑣 ) )
11 cnfcom3c.n ⊢ 𝑁 = ( ( 𝑋 ∘ ◡ 𝑌 ) ∘ ( 𝑇 ‘ dom 𝐺 ) )
12 cnfcom3c.l ⊢ 𝐿 = ( 𝑏 ∈ ( ω ↑o 𝐴 ) ↦ 𝑁 )
13 simp1 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝐴 ∈ On )
14 omelon ⊢ ω ∈ On
15 1onn ⊢ 1o ∈ ω
16 ondif2 ⊢ ( ω ∈ ( On ∖ 2o ) ↔ ( ω ∈ On ∧ 1o ∈ ω ) )
17 14 15 16 mpbir2an ⊢ ω ∈ ( On ∖ 2o )
18 oeworde ⊢ ( ( ω ∈ ( On ∖ 2o ) ∧ 𝐴 ∈ On ) → 𝐴 ⊆ ( ω ↑o 𝐴 ) )
19 17 13 18 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝐴 ⊆ ( ω ↑o 𝐴 ) )
20 simp2 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑏 ∈ 𝐴 )
21 19 20 sseldd ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑏 ∈ ( ω ↑o 𝐴 ) )
22 simp3 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → ω ⊆ 𝑏 )
23 1 13 21 2 3 4 5 6 7 8 22 cnfcom3lem ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑊 ∈ ( On ∖ 1o ) )
24 1 13 21 2 3 4 5 6 7 8 22 9 10 11 cnfcom3 ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑁 : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) )
25 f1of ⊢ ( 𝑁 : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) → 𝑁 : 𝑏 ⟶ ( ω ↑o 𝑊 ) )
26 24 25 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑁 : 𝑏 ⟶ ( ω ↑o 𝑊 ) )
27 vex ⊢ 𝑏 ∈ V
28 fex ⊢ ( ( 𝑁 : 𝑏 ⟶ ( ω ↑o 𝑊 ) ∧ 𝑏 ∈ V ) → 𝑁 ∈ V )
29 26 27 28 sylancl ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → 𝑁 ∈ V )
30 12 fvmpt2 ⊢ ( ( 𝑏 ∈ ( ω ↑o 𝐴 ) ∧ 𝑁 ∈ V ) → ( 𝐿 ‘ 𝑏 ) = 𝑁 )
31 21 29 30 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → ( 𝐿 ‘ 𝑏 ) = 𝑁 )
32 f1oeq1 ⊢ ( ( 𝐿 ‘ 𝑏 ) = 𝑁 → ( ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ 𝑁 : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
33 31 32 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → ( ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ↔ 𝑁 : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
34 24 33 mpbird ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) )
35 oveq2 ⊢ ( 𝑤 = 𝑊 → ( ω ↑o 𝑤 ) = ( ω ↑o 𝑊 ) )
36 35 f1oeq3d ⊢ ( 𝑤 = 𝑊 → ( ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) )
37 36 rspcev ⊢ ( ( 𝑊 ∈ ( On ∖ 1o ) ∧ ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑊 ) ) → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) )
38 23 34 37 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏 ) → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) )
39 38 3expia ⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
40 39 ralrimiva ⊢ ( 𝐴 ∈ On → ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
41 ovex ⊢ ( ω ↑o 𝐴 ) ∈ V
42 41 mptex ⊢ ( 𝑏 ∈ ( ω ↑o 𝐴 ) ↦ 𝑁 ) ∈ V
43 12 42 eqeltri ⊢ 𝐿 ∈ V
44 nfmpt1 ⊢ Ⅎ 𝑏 ( 𝑏 ∈ ( ω ↑o 𝐴 ) ↦ 𝑁 )
45 12 44 nfcxfr ⊢ Ⅎ 𝑏 𝐿
46 45 nfeq2 ⊢ Ⅎ 𝑏 𝑔 = 𝐿
47 fveq1 ⊢ ( 𝑔 = 𝐿 → ( 𝑔 ‘ 𝑏 ) = ( 𝐿 ‘ 𝑏 ) )
48 f1oeq1 ⊢ ( ( 𝑔 ‘ 𝑏 ) = ( 𝐿 ‘ 𝑏 ) → ( ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
49 47 48 syl ⊢ ( 𝑔 = 𝐿 → ( ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
50 49 rexbidv ⊢ ( 𝑔 = 𝐿 → ( ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ↔ ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
51 50 imbi2d ⊢ ( 𝑔 = 𝐿 → ( ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ↔ ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) )
52 46 51 ralbid ⊢ ( 𝑔 = 𝐿 → ( ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) ) )
53 43 52 spcev ⊢ ( ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝐿 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )
54 40 53 syl ⊢ ( 𝐴 ∈ On → ∃ 𝑔 ∀ 𝑏 ∈ 𝐴 ( ω ⊆ 𝑏 → ∃ 𝑤 ∈ ( On ∖ 1o ) ( 𝑔 ‘ 𝑏 ) : 𝑏 –1-1-onto→ ( ω ↑o 𝑤 ) ) )