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 ⊢ S = dom ⁡ ω CNF A
cnfcom3c.f ⊢ F = ω CNF A -1 ⁡ b
cnfcom3c.g ⊢ G = OrdIso E F supp ∅
cnfcom3c.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ M + 𝑜 z ∅
cnfcom3c.t ⊢ T = seq ω k ∈ V , f ∈ V ⟼ K ∅
cnfcom3c.m ⊢ M = ω ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k
cnfcom3c.k ⊢ K = x ∈ M ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ M + 𝑜 x -1
cnfcom3c.w ⊢ W = G ⁡ ⋃ dom ⁡ G
cnfcom3c.x ⊢ X = u ∈ F ⁡ W , v ∈ ω ↑ 𝑜 W ⟼ F ⁡ W ⋅ 𝑜 v + 𝑜 u
cnfcom3c.y ⊢ Y = u ∈ F ⁡ W , v ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 u + 𝑜 v
cnfcom3c.n ⊢ N = X ∘ Y -1 ∘ T ⁡ dom ⁡ G
cnfcom3c.l ⊢ L = b ∈ ω ↑ 𝑜 A ⟼ N
Assertion cnfcom3clem ⊢ A ∈ On → ∃ g ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w

Proof

Step Hyp Ref Expression
1 cnfcom3c.s ⊢ S = dom ⁡ ω CNF A
2 cnfcom3c.f ⊢ F = ω CNF A -1 ⁡ b
3 cnfcom3c.g ⊢ G = OrdIso E F supp ∅
4 cnfcom3c.h ⊢ H = seq ω k ∈ V , z ∈ V ⟼ M + 𝑜 z ∅
5 cnfcom3c.t ⊢ T = seq ω k ∈ V , f ∈ V ⟼ K ∅
6 cnfcom3c.m ⊢ M = ω ↑ 𝑜 G ⁡ k ⋅ 𝑜 F ⁡ G ⁡ k
7 cnfcom3c.k ⊢ K = x ∈ M ⟼ dom ⁡ f + 𝑜 x ∪ x ∈ dom ⁡ f ⟼ M + 𝑜 x -1
8 cnfcom3c.w ⊢ W = G ⁡ ⋃ dom ⁡ G
9 cnfcom3c.x ⊢ X = u ∈ F ⁡ W , v ∈ ω ↑ 𝑜 W ⟼ F ⁡ W ⋅ 𝑜 v + 𝑜 u
10 cnfcom3c.y ⊢ Y = u ∈ F ⁡ W , v ∈ ω ↑ 𝑜 W ⟼ ω ↑ 𝑜 W ⋅ 𝑜 u + 𝑜 v
11 cnfcom3c.n ⊢ N = X ∘ Y -1 ∘ T ⁡ dom ⁡ G
12 cnfcom3c.l ⊢ L = b ∈ ω ↑ 𝑜 A ⟼ N
13 simp1 ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → A ∈ On
14 omelon ⊢ ω ∈ On
15 1onn ⊢ 1 𝑜 ∈ ω
16 ondif2 ⊢ ω ∈ On ∖ 2 𝑜 ↔ ω ∈ On ∧ 1 𝑜 ∈ ω
17 14 15 16 mpbir2an ⊢ ω ∈ On ∖ 2 𝑜
18 oeworde ⊢ ω ∈ On ∖ 2 𝑜 ∧ A ∈ On → A ⊆ ω ↑ 𝑜 A
19 17 13 18 sylancr ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → A ⊆ ω ↑ 𝑜 A
20 simp2 ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → b ∈ A
21 19 20 sseldd ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → b ∈ ω ↑ 𝑜 A
22 simp3 ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → ω ⊆ b
23 1 13 21 2 3 4 5 6 7 8 22 cnfcom3lem ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → W ∈ On ∖ 1 𝑜
24 1 13 21 2 3 4 5 6 7 8 22 9 10 11 cnfcom3 ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → N : b ⟶ 1-1 onto ω ↑ 𝑜 W
25 f1of ⊢ N : b ⟶ 1-1 onto ω ↑ 𝑜 W → N : b ⟶ ω ↑ 𝑜 W
26 24 25 syl ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → N : b ⟶ ω ↑ 𝑜 W
27 vex ⊢ b ∈ V
28 fex ⊢ N : b ⟶ ω ↑ 𝑜 W ∧ b ∈ V → N ∈ V
29 26 27 28 sylancl ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → N ∈ V
30 12 fvmpt2 ⊢ b ∈ ω ↑ 𝑜 A ∧ N ∈ V → L ⁡ b = N
31 21 29 30 syl2anc ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → L ⁡ b = N
32 f1oeq1 ⊢ L ⁡ b = N → L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 W ↔ N : b ⟶ 1-1 onto ω ↑ 𝑜 W
33 31 32 syl ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 W ↔ N : b ⟶ 1-1 onto ω ↑ 𝑜 W
34 24 33 mpbird ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 W
35 oveq2 ⊢ w = W → ω ↑ 𝑜 w = ω ↑ 𝑜 W
36 35 f1oeq3d ⊢ w = W → L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 W
37 36 rspcev ⊢ W ∈ On ∖ 1 𝑜 ∧ L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 W → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
38 23 34 37 syl2anc ⊢ A ∈ On ∧ b ∈ A ∧ ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
39 38 3expia ⊢ A ∈ On ∧ b ∈ A → ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
40 39 ralrimiva ⊢ A ∈ On → ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
41 ovex ⊢ ω ↑ 𝑜 A ∈ V
42 41 mptex ⊢ b ∈ ω ↑ 𝑜 A ⟼ N ∈ V
43 12 42 eqeltri ⊢ L ∈ V
44 nfmpt1 ⊢ Ⅎ _ b b ∈ ω ↑ 𝑜 A ⟼ N
45 12 44 nfcxfr ⊢ Ⅎ _ b L
46 45 nfeq2 ⊢ Ⅎ b g = L
47 fveq1 ⊢ g = L → g ⁡ b = L ⁡ b
48 f1oeq1 ⊢ g ⁡ b = L ⁡ b → g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
49 47 48 syl ⊢ g = L → g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
50 49 rexbidv ⊢ g = L → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
51 50 imbi2d ⊢ g = L → ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
52 46 51 ralbid ⊢ g = L → ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w ↔ ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
53 43 52 spcev ⊢ ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 L ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w → ∃ g ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w
54 40 53 syl ⊢ A ∈ On → ∃ g ∀ b ∈ A ω ⊆ b → ∃ w ∈ On ∖ 1 𝑜 g ⁡ b : b ⟶ 1-1 onto ω ↑ 𝑜 w