Metamath Proof Explorer

Theorem cantnfp1lem2

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 30-Jun-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfp1.g ⊢ φ → G ∈ S
cantnfp1.x ⊢ φ → X ∈ B
cantnfp1.y ⊢ φ → Y ∈ A
cantnfp1.s ⊢ φ → G supp ∅ ⊆ X
cantnfp1.f ⊢ F = t ∈ B ⟼ if t = X Y G ⁡ t
cantnfp1.e ⊢ φ → ∅ ∈ Y
cantnfp1.o ⊢ O = OrdIso E F supp ∅
Assertion cantnfp1lem2 ⊢ φ → dom ⁡ O = suc ⁡ ⋃ dom ⁡ O

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnfp1.g ⊢ φ → G ∈ S
5 cantnfp1.x ⊢ φ → X ∈ B
6 cantnfp1.y ⊢ φ → Y ∈ A
7 cantnfp1.s ⊢ φ → G supp ∅ ⊆ X
8 cantnfp1.f ⊢ F = t ∈ B ⟼ if t = X Y G ⁡ t
9 cantnfp1.e ⊢ φ → ∅ ∈ Y
10 cantnfp1.o ⊢ O = OrdIso E F supp ∅
11 iftrue ⊢ t = X → if t = X Y G ⁡ t = Y
12 8 11 5 6 fvmptd3 ⊢ φ → F ⁡ X = Y
13 9 ne0d ⊢ φ → Y ≠ ∅
14 12 13 eqnetrd ⊢ φ → F ⁡ X ≠ ∅
15 6 adantr ⊢ φ ∧ t ∈ B → Y ∈ A
16 1 2 3 cantnfs ⊢ φ → G ∈ S ↔ G : B ⟶ A ∧ finSupp ∅⁡ G
17 4 16 mpbid ⊢ φ → G : B ⟶ A ∧ finSupp ∅⁡ G
18 17 simpld ⊢ φ → G : B ⟶ A
19 18 ffvelrnda ⊢ φ ∧ t ∈ B → G ⁡ t ∈ A
20 15 19 ifcld ⊢ φ ∧ t ∈ B → if t = X Y G ⁡ t ∈ A
21 20 8 fmptd ⊢ φ → F : B ⟶ A
22 21 ffnd ⊢ φ → F Fn B
23 9 elexd ⊢ φ → ∅ ∈ V
24 elsuppfn ⊢ F Fn B ∧ B ∈ On ∧ ∅ ∈ V → X ∈ supp ∅⁡ F ↔ X ∈ B ∧ F ⁡ X ≠ ∅
25 22 3 23 24 syl3anc ⊢ φ → X ∈ supp ∅⁡ F ↔ X ∈ B ∧ F ⁡ X ≠ ∅
26 5 14 25 mpbir2and ⊢ φ → X ∈ supp ∅⁡ F
27 n0i ⊢ X ∈ supp ∅⁡ F → ¬ F supp ∅ = ∅
28 26 27 syl ⊢ φ → ¬ F supp ∅ = ∅
29 ovexd ⊢ φ → F supp ∅ ∈ V
30 1 2 3 4 5 6 7 8 cantnfp1lem1 ⊢ φ → F ∈ S
31 1 2 3 10 30 cantnfcl ⊢ φ → E We supp ∅⁡ F ∧ dom ⁡ O ∈ ω
32 31 simpld ⊢ φ → E We supp ∅⁡ F
33 10 oien ⊢ F supp ∅ ∈ V ∧ E We supp ∅⁡ F → dom ⁡ O ≈ supp ∅⁡ F
34 29 32 33 syl2anc ⊢ φ → dom ⁡ O ≈ supp ∅⁡ F
35 breq1 ⊢ dom ⁡ O = ∅ → dom ⁡ O ≈ supp ∅⁡ F ↔ ∅ ≈ supp ∅⁡ F
36 ensymb ⊢ ∅ ≈ supp ∅⁡ F ↔ supp ∅⁡ F ≈ ∅
37 en0 ⊢ supp ∅⁡ F ≈ ∅ ↔ F supp ∅ = ∅
38 36 37 bitri ⊢ ∅ ≈ supp ∅⁡ F ↔ F supp ∅ = ∅
39 35 38 bitrdi ⊢ dom ⁡ O = ∅ → dom ⁡ O ≈ supp ∅⁡ F ↔ F supp ∅ = ∅
40 34 39 syl5ibcom ⊢ φ → dom ⁡ O = ∅ → F supp ∅ = ∅
41 28 40 mtod ⊢ φ → ¬ dom ⁡ O = ∅
42 31 simprd ⊢ φ → dom ⁡ O ∈ ω
43 nnlim ⊢ dom ⁡ O ∈ ω → ¬ Lim ⁡ dom ⁡ O
44 42 43 syl ⊢ φ → ¬ Lim ⁡ dom ⁡ O
45 ioran ⊢ ¬ dom ⁡ O = ∅ ∨ Lim ⁡ dom ⁡ O ↔ ¬ dom ⁡ O = ∅ ∧ ¬ Lim ⁡ dom ⁡ O
46 41 44 45 sylanbrc ⊢ φ → ¬ dom ⁡ O = ∅ ∨ Lim ⁡ dom ⁡ O
47 nnord ⊢ dom ⁡ O ∈ ω → Ord ⁡ dom ⁡ O
48 unizlim ⊢ Ord ⁡ dom ⁡ O → dom ⁡ O = ⋃ dom ⁡ O ↔ dom ⁡ O = ∅ ∨ Lim ⁡ dom ⁡ O
49 42 47 48 3syl ⊢ φ → dom ⁡ O = ⋃ dom ⁡ O ↔ dom ⁡ O = ∅ ∨ Lim ⁡ dom ⁡ O
50 46 49 mtbird ⊢ φ → ¬ dom ⁡ O = ⋃ dom ⁡ O
51 orduniorsuc ⊢ Ord ⁡ dom ⁡ O → dom ⁡ O = ⋃ dom ⁡ O ∨ dom ⁡ O = suc ⁡ ⋃ dom ⁡ O
52 42 47 51 3syl ⊢ φ → dom ⁡ O = ⋃ dom ⁡ O ∨ dom ⁡ O = suc ⁡ ⋃ dom ⁡ O
53 52 ord ⊢ φ → ¬ dom ⁡ O = ⋃ dom ⁡ O → dom ⁡ O = suc ⁡ ⋃ dom ⁡ O
54 50 53 mpd ⊢ φ → dom ⁡ O = suc ⁡ ⋃ dom ⁡ O