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 ffvelrnda ( ( 𝜑𝑡𝐵 ) → ( 𝐺𝑡 ) ∈ 𝐴 )
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 𝑂 )