This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnfp1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
cantnfp1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
cantnfp1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
cantnfp1.s ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝑋 )
cantnfp1.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐵 ↦ if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) )
cantnfp1.e ⊢ ( 𝜑 → ∅ ∈ 𝑌 )
cantnfp1.o ⊢ 𝑂 = OrdIso ( E , ( 𝐹 supp ∅ ) )
Assertion cantnfp1lem2 ( 𝜑 → dom 𝑂 = suc ∪ dom 𝑂 )

Proof

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