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

Metamath Proof Explorer

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 ( ◡ 𝑂 ‘ 𝑋 ) ) )