Theorem cantnflem1d

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

	Ref	Expression
Hypotheses	cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	oemapval.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
	oemapval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
	oemapval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
	oemapvali.r	⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
	oemapvali.x	⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
	cantnflem1.o	⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
	cantnflem1.h	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
Assertion	cantnflem1d	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		oemapval.t	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐵 ( ( 𝑥 ‘ 𝑧 ) ∈ ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
5		oemapval.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6		oemapval.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑆 )
7		oemapvali.r	⊢ ( 𝜑 → 𝐹 𝑇 𝐺 )
8		oemapvali.x	⊢ 𝑋 = ∪ { 𝑐 ∈ 𝐵 ∣ ( 𝐹 ‘ 𝑐 ) ∈ ( 𝐺 ‘ 𝑐 ) }
9		cantnflem1.o	⊢ 𝑂 = OrdIso ( E , ( 𝐺 supp ∅ ) )
10		cantnflem1.h	⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
11	1 2 3 4 5 6 7 8	oemapvali	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
12	11	simp1d	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
13		onelon	⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
14	3 12 13	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ On )
15		oecl	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ On ) → ( 𝐴 ↑o 𝑋 ) ∈ On )
16	2 14 15	syl2anc	⊢ ( 𝜑 → ( 𝐴 ↑o 𝑋 ) ∈ On )
17	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
18	6 17	mpbid	⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
19	18	simpld	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
20	19 12	ffvelcdmd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
21		onelon	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ On )
22	2 20 21	syl2anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ On )
23		omcl	⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( 𝐺 ‘ 𝑋 ) ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ∈ On )
24	16 22 23	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ∈ On )
25		ovexd	⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ∈ V )
26	1 2 3 9 6	cantnfcl	⊢ ( 𝜑 → ( E We ( 𝐺 supp ∅ ) ∧ dom 𝑂 ∈ ω ) )
27	26	simpld	⊢ ( 𝜑 → E We ( 𝐺 supp ∅ ) )
28	9	oiiso	⊢ ( ( ( 𝐺 supp ∅ ) ∈ V ∧ E We ( 𝐺 supp ∅ ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
29	25 27 28	syl2anc	⊢ ( 𝜑 → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
30		isof1o	⊢ ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
31	29 30	syl	⊢ ( 𝜑 → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
32		f1ocnv	⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) → ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 )
33		f1of	⊢ ( ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
34	31 32 33	3syl	⊢ ( 𝜑 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
35	1 2 3 4 5 6 7 8	cantnflem1a	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) )
36	34 35	ffvelcdmd	⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
37	26	simprd	⊢ ( 𝜑 → dom 𝑂 ∈ ω )
38		elnn	⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ ω )
39	36 37 38	syl2anc	⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ ω )
40	10	cantnfvalf	⊢ 𝐻 : ω ⟶ On
41	40	ffvelcdmi	⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ ω → ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ On )
42	39 41	syl	⊢ ( 𝜑 → ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ On )
43		oaword1	⊢ ( ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ∈ On ∧ ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
44	24 42 43	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ⊆ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
45	1 2 3 9 6 10	cantnfsuc	⊢ ( ( 𝜑 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ ω ) → ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
46	39 45	mpdan	⊢ ( 𝜑 → ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
47		f1ocnvfv2	⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) ∧ 𝑋 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
48	31 35 47	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
49	48	oveq2d	⊢ ( 𝜑 → ( 𝐴 ↑o ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) = ( 𝐴 ↑o 𝑋 ) )
50	48	fveq2d	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) = ( 𝐺 ‘ 𝑋 ) )
51	49 50	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 ↑o ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ) = ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) )
52	51	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑o ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
53	46 52	eqtrd	⊢ ( 𝜑 → ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) +o ( 𝐻 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
54	44 53	sseqtrrd	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ⊆ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) )
55		onss	⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
56	3 55	syl	⊢ ( 𝜑 → 𝐵 ⊆ On )
57	56	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
58	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑋 ∈ On )
59		onsseleq	⊢ ( ( 𝑥 ∈ On ∧ 𝑋 ∈ On ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
60	57 58 59	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ) )
61		orcom	⊢ ( ( 𝑥 ∈ 𝑋 ∨ 𝑥 = 𝑋 ) ↔ ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) )
62	60 61	bitrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ 𝑋 ↔ ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) ) )
63	62	ifbid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
64	63	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
65	64	fveq2d	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
66	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
67	5 66	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) )
68	67	simpld	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
69	68	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐴 )
70	20	ne0d	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
71		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
72	2 71	syl	⊢ ( 𝜑 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
73	70 72	mpbird	⊢ ( 𝜑 → ∅ ∈ 𝐴 )
74	73	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ 𝐴 )
75	69 74	ifcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ∈ 𝐴 )
76	75	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) : 𝐵 ⟶ 𝐴 )
77		0ex	⊢ ∅ ∈ V
78	77	a1i	⊢ ( 𝜑 → ∅ ∈ V )
79	67	simprd	⊢ ( 𝜑 → 𝐹 finSupp ∅ )
80	68 3 78 79	fsuppmptif	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) finSupp ∅ )
81	1 2 3	cantnfs	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ∈ 𝑆 ↔ ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) : 𝐵 ⟶ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) finSupp ∅ ) ) )
82	76 80 81	mpbir2and	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ∈ 𝑆 )
83	68 12	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ 𝐴 )
84		eldifn	⊢ ( 𝑦 ∈ ( 𝐵 ∖ 𝑋 ) → ¬ 𝑦 ∈ 𝑋 )
85	84	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑋 ) ) → ¬ 𝑦 ∈ 𝑋 )
86	85	iffalsed	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐵 ∖ 𝑋 ) ) → if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) = ∅ )
87	86 3	suppss2	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) supp ∅ ) ⊆ 𝑋 )
88		ifor	⊢ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑥 ) , if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
89		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
90	89	adantl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑥 = 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑋 ) )
91	90	ifeq1da	⊢ ( 𝑥 ∈ 𝐵 → if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑥 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) = if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑋 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) )
92		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝑋 ↔ 𝑥 ∈ 𝑋 ) )
93		fveq2	⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
94	92 93	ifbieq1d	⊢ ( 𝑦 = 𝑥 → if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) = if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
95		eqid	⊢ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
96		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
97	96 77	ifex	⊢ if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V
98	94 95 97	fvmpt	⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) = if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
99	98	ifeq2d	⊢ ( 𝑥 ∈ 𝐵 → if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑥 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) = if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑥 ) , if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
100	91 99	eqtr3d	⊢ ( 𝑥 ∈ 𝐵 → if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑋 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) = if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑥 ) , if ( 𝑥 ∈ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
101	88 100	eqtr4id	⊢ ( 𝑥 ∈ 𝐵 → if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑋 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) )
102	101	mpteq2ia	⊢ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 = 𝑋 , ( 𝐹 ‘ 𝑋 ) , ( ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ‘ 𝑥 ) ) )
103	1 2 3 82 12 83 87 102	cantnfp1	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) ) )
104	103	simprd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = 𝑋 ∨ 𝑥 ∈ 𝑋 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) )
105	65 104	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) )
106		onelon	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐹 ‘ 𝑋 ) ∈ 𝐴 ) → ( 𝐹 ‘ 𝑋 ) ∈ On )
107	2 83 106	syl2anc	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ On )
108		omsuc	⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( 𝐹 ‘ 𝑋 ) ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o suc ( 𝐹 ‘ 𝑋 ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) )
109	16 107 108	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o suc ( 𝐹 ‘ 𝑋 ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) )
110		eloni	⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ On → Ord ( 𝐺 ‘ 𝑋 ) )
111	22 110	syl	⊢ ( 𝜑 → Ord ( 𝐺 ‘ 𝑋 ) )
112	11	simp2d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) )
113		ordsucss	⊢ ( Ord ( 𝐺 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) → suc ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐺 ‘ 𝑋 ) ) )
114	111 112 113	sylc	⊢ ( 𝜑 → suc ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐺 ‘ 𝑋 ) )
115		onsuc	⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ On → suc ( 𝐹 ‘ 𝑋 ) ∈ On )
116	107 115	syl	⊢ ( 𝜑 → suc ( 𝐹 ‘ 𝑋 ) ∈ On )
117		omwordi	⊢ ( ( suc ( 𝐹 ‘ 𝑋 ) ∈ On ∧ ( 𝐺 ‘ 𝑋 ) ∈ On ∧ ( 𝐴 ↑o 𝑋 ) ∈ On ) → ( suc ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐺 ‘ 𝑋 ) → ( ( 𝐴 ↑o 𝑋 ) ·o suc ( 𝐹 ‘ 𝑋 ) ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ) )
118	116 22 16 117	syl3anc	⊢ ( 𝜑 → ( suc ( 𝐹 ‘ 𝑋 ) ⊆ ( 𝐺 ‘ 𝑋 ) → ( ( 𝐴 ↑o 𝑋 ) ·o suc ( 𝐹 ‘ 𝑋 ) ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) ) )
119	114 118	mpd	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o suc ( 𝐹 ‘ 𝑋 ) ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) )
120	109 119	eqsstrrd	⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) ⊆ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) )
121	1 2 3 82 73 14 87	cantnflt2	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝑋 ) )
122		onelon	⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝑋 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ On )
123	16 121 122	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ On )
124		omcl	⊢ ( ( ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( 𝐹 ‘ 𝑋 ) ∈ On ) → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) ∈ On )
125	16 107 124	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) ∈ On )
126		oaord	⊢ ( ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ On ∧ ( 𝐴 ↑o 𝑋 ) ∈ On ∧ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) ∈ On ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝑋 ) ↔ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) ) )
127	123 16 125 126	syl3anc	⊢ ( 𝜑 → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝑋 ) ↔ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) ) )
128	121 127	mpbid	⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( 𝐴 ↑o 𝑋 ) ) )
129	120 128	sseldd	⊢ ( 𝜑 → ( ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐹 ‘ 𝑋 ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 ∈ 𝑋 , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) ) ) ∈ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) )
130	105 129	eqeltrd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( ( 𝐴 ↑o 𝑋 ) ·o ( 𝐺 ‘ 𝑋 ) ) )
131	54 130	sseldd	⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) )