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 𝑂 )