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

Metamath Proof Explorer

Theorem cantnfp1lem3

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-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 ∅ ) )
cantnfp1.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
cantnfp1.k ⊢ 𝐾 = OrdIso ( E , ( 𝐺 supp ∅ ) )
cantnfp1.m ⊢ 𝑀 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
Assertion cantnfp1lem3 ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )

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 cantnfp1.h ⊢ 𝐻 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
12 cantnfp1.k ⊢ 𝐾 = OrdIso ( E , ( 𝐺 supp ∅ ) )
13 cantnfp1.m ⊢ 𝑀 = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑘 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
14 1 2 3 4 5 6 7 8 cantnfp1lem1 ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
15 1 2 3 10 14 11 cantnfval ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( 𝐻 ‘ dom 𝑂 ) )
16 1 2 3 4 5 6 7 8 9 10 cantnfp1lem2 ⊢ ( 𝜑 → dom 𝑂 = suc ∪ dom 𝑂 )
17 16 fveq2d ⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝑂 ) = ( 𝐻 ‘ suc ∪ dom 𝑂 ) )
18 1 2 3 10 14 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝑂 ∈ ω ) )
19 18 simprd ⊢ ( 𝜑 → dom 𝑂 ∈ ω )
20 16 19 eqeltrrd ⊢ ( 𝜑 → suc ∪ dom 𝑂 ∈ ω )
21 peano2b ⊢ ( ∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω )
22 20 21 sylibr ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ ω )
23 1 2 3 10 14 11 cantnfsuc ⊢ ( ( 𝜑 ∧ ∪ dom 𝑂 ∈ ω ) → ( 𝐻 ‘ suc ∪ dom 𝑂 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ ∪ dom 𝑂 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) +o ( 𝐻 ‘ ∪ dom 𝑂 ) ) )
24 22 23 mpdan ⊢ ( 𝜑 → ( 𝐻 ‘ suc ∪ dom 𝑂 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ ∪ dom 𝑂 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) +o ( 𝐻 ‘ ∪ dom 𝑂 ) ) )
25 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
26 18 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
27 10 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐹 supp ∅ ) ) )
28 25 26 27 syl2anc ⊢ ( 𝜑 → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐹 supp ∅ ) ) )
29 isof1o ⊢ ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐹 supp ∅ ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) )
30 28 29 syl ⊢ ( 𝜑 → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) )
31 f1ocnv ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) → ◡ 𝑂 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝑂 )
32 f1of ⊢ ( ◡ 𝑂 : ( 𝐹 supp ∅ ) –1-1-onto→ dom 𝑂 → ◡ 𝑂 : ( 𝐹 supp ∅ ) ⟶ dom 𝑂 )
33 30 31 32 3syl ⊢ ( 𝜑 → ◡ 𝑂 : ( 𝐹 supp ∅ ) ⟶ dom 𝑂 )
34 iftrue ⊢ ( 𝑡 = 𝑋 → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) = 𝑌 )
35 8 34 5 6 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 𝑌 )
36 9 ne0d ⊢ ( 𝜑 → 𝑌 ≠ ∅ )
37 35 36 eqnetrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ ∅ )
38 6 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → 𝑌 ∈ 𝐴 )
39 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
40 4 39 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
41 40 simpld ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
42 41 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑡 ) ∈ 𝐴 )
43 38 42 ifcld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐵 ) → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) ∈ 𝐴 )
44 43 8 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
45 44 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
46 0ex ⊢ ∅ ∈ V
47 46 a1i ⊢ ( 𝜑 → ∅ ∈ V )
48 elsuppfn ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) ) )
49 45 3 47 48 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐹 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ≠ ∅ ) ) )
50 5 37 49 mpbir2and ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐹 supp ∅ ) )
51 33 50 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
52 elssuni ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 )
53 51 52 syl ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 )
54 10 oicl ⊢ Ord dom 𝑂
55 ordelon ⊢ ( ( Ord dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
56 54 51 55 sylancr ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
57 nnon ⊢ ( ∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ On )
58 22 57 syl ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ On )
59 ontri1 ⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On ∧ ∪ dom 𝑂 ∈ On ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
60 56 58 59 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
61 53 60 mpbid ⊢ ( 𝜑 → ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
62 sucidg ⊢ ( ∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂 )
63 22 62 syl ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂 )
64 63 16 eleqtrrd ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ dom 𝑂 )
65 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐹 supp ∅ ) ) ∧ ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) ) → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
66 28 64 51 65 syl12anc ⊢ ( 𝜑 → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
67 fvex ⊢ ( ◡ 𝑂 ‘ 𝑋 ) ∈ V
68 67 epeli ⊢ ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
69 fvex ⊢ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ V
70 69 epeli ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) )
71 66 68 70 3bitr3g ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
72 f1ocnvfv2 ⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) ∧ 𝑋 ∈ ( 𝐹 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
73 30 50 72 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
74 73 eleq2d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
75 71 74 bitrd ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
76 61 75 mtbid ⊢ ( 𝜑 → ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 )
77 7 sseld ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
78 suppssdm ⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
79 78 44 fssdm ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐵 )
80 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
81 3 80 syl ⊢ ( 𝜑 → 𝐵 ⊆ On )
82 79 81 sstrd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ On )
83 10 oif ⊢ 𝑂 : dom 𝑂 ⟶ ( 𝐹 supp ∅ )
84 83 ffvelcdmi ⊢ ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐹 supp ∅ ) )
85 64 84 syl ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐹 supp ∅ ) )
86 82 85 sseldd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On )
87 eloni ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On → Ord ( 𝑂 ‘ ∪ dom 𝑂 ) )
88 86 87 syl ⊢ ( 𝜑 → Ord ( 𝑂 ‘ ∪ dom 𝑂 ) )
89 ordn2lp ⊢ ( Ord ( 𝑂 ‘ ∪ dom 𝑂 ) → ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∧ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
90 88 89 syl ⊢ ( 𝜑 → ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∧ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
91 imnan ⊢ ( ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 → ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ↔ ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∧ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
92 90 91 sylibr ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 → ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
93 77 92 syld ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) → ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
94 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
95 3 5 94 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ On )
96 eloni ⊢ ( 𝑋 ∈ On → Ord 𝑋 )
97 95 96 syl ⊢ ( 𝜑 → Ord 𝑋 )
98 ordirr ⊢ ( Ord 𝑋 → ¬ 𝑋 ∈ 𝑋 )
99 97 98 syl ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑋 )
100 elsni ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } → ( 𝑂 ‘ ∪ dom 𝑂 ) = 𝑋 )
101 100 eleq2d ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } → ( 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ 𝑋 ∈ 𝑋 ) )
102 101 notbid ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } → ( ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ ¬ 𝑋 ∈ 𝑋 ) )
103 99 102 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } → ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
104 eqeq1 ⊢ ( 𝑡 = 𝑘 → ( 𝑡 = 𝑋 ↔ 𝑘 = 𝑋 ) )
105 fveq2 ⊢ ( 𝑡 = 𝑘 → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ 𝑘 ) )
106 104 105 ifbieq2d ⊢ ( 𝑡 = 𝑘 → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) = if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) )
107 eldifi ⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → 𝑘 ∈ 𝐵 )
108 107 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → 𝑘 ∈ 𝐵 )
109 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → 𝑌 ∈ 𝐴 )
110 fvex ⊢ ( 𝐺 ‘ 𝑘 ) ∈ V
111 ifexg ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐺 ‘ 𝑘 ) ∈ V ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ∈ V )
112 109 110 111 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ∈ V )
113 8 106 108 112 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) )
114 eldifn ⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → ¬ 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
115 114 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ¬ 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
116 velsn ⊢ ( 𝑘 ∈ { 𝑋 } ↔ 𝑘 = 𝑋 )
117 elun2 ⊢ ( 𝑘 ∈ { 𝑋 } → 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
118 116 117 sylbir ⊢ ( 𝑘 = 𝑋 → 𝑘 ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
119 115 118 nsyl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ¬ 𝑘 = 𝑋 )
120 119 iffalsed ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
121 ssun1 ⊢ ( 𝐺 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } )
122 sscon ⊢ ( ( 𝐺 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) → ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ⊆ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) )
123 121 122 ax-mp ⊢ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ⊆ ( 𝐵 ∖ ( 𝐺 supp ∅ ) )
124 123 sseli ⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) → 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) )
125 ssidd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ ( 𝐺 supp ∅ ) )
126 41 125 3 9 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) ) → ( 𝐺 ‘ 𝑘 ) = ∅ )
127 124 126 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐺 ‘ 𝑘 ) = ∅ )
128 113 120 127 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ) ) → ( 𝐹 ‘ 𝑘 ) = ∅ )
129 44 128 suppss ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
130 129 85 sseldd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) )
131 elun ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) ↔ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) ∨ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } ) )
132 130 131 sylib ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) ∨ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ { 𝑋 } ) )
133 93 103 132 mpjaod ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) )
134 ioran ⊢ ( ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∨ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ↔ ( ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∧ ¬ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
135 76 133 134 sylanbrc ⊢ ( 𝜑 → ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∨ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
136 ordtri3 ⊢ ( ( Ord ( 𝑂 ‘ ∪ dom 𝑂 ) ∧ Ord 𝑋 ) → ( ( 𝑂 ‘ ∪ dom 𝑂 ) = 𝑋 ↔ ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∨ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) )
137 88 97 136 syl2anc ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) = 𝑋 ↔ ¬ ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ∨ 𝑋 ∈ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) )
138 135 137 mpbird ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) = 𝑋 )
139 138 oveq2d ⊢ ( 𝜑 → ( 𝐴 ↑o ( 𝑂 ‘ ∪ dom 𝑂 ) ) = ( 𝐴 ↑o 𝑋 ) )
140 138 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) = ( 𝐹 ‘ 𝑋 ) )
141 140 35 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) = 𝑌 )
142 139 141 oveq12d ⊢ ( 𝜑 → ( ( 𝐴 ↑o ( 𝑂 ‘ ∪ dom 𝑂 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) = ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) )
143 nnord ⊢ ( ∪ dom 𝑂 ∈ ω → Ord ∪ dom 𝑂 )
144 22 143 syl ⊢ ( 𝜑 → Ord ∪ dom 𝑂 )
145 sssucid ⊢ ∪ dom 𝑂 ⊆ suc ∪ dom 𝑂
146 145 16 sseqtrrid ⊢ ( 𝜑 → ∪ dom 𝑂 ⊆ dom 𝑂 )
147 f1ofo ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) → 𝑂 : dom 𝑂 –onto→ ( 𝐹 supp ∅ ) )
148 30 147 syl ⊢ ( 𝜑 → 𝑂 : dom 𝑂 –onto→ ( 𝐹 supp ∅ ) )
149 foima ⊢ ( 𝑂 : dom 𝑂 –onto→ ( 𝐹 supp ∅ ) → ( 𝑂 “ dom 𝑂 ) = ( 𝐹 supp ∅ ) )
150 148 149 syl ⊢ ( 𝜑 → ( 𝑂 “ dom 𝑂 ) = ( 𝐹 supp ∅ ) )
151 ffn ⊢ ( 𝑂 : dom 𝑂 ⟶ ( 𝐹 supp ∅ ) → 𝑂 Fn dom 𝑂 )
152 83 151 ax-mp ⊢ 𝑂 Fn dom 𝑂
153 fnsnfv ⊢ ( ( 𝑂 Fn dom 𝑂 ∧ ∪ dom 𝑂 ∈ dom 𝑂 ) → { ( 𝑂 ‘ ∪ dom 𝑂 ) } = ( 𝑂 “ { ∪ dom 𝑂 } ) )
154 152 64 153 sylancr ⊢ ( 𝜑 → { ( 𝑂 ‘ ∪ dom 𝑂 ) } = ( 𝑂 “ { ∪ dom 𝑂 } ) )
155 138 sneqd ⊢ ( 𝜑 → { ( 𝑂 ‘ ∪ dom 𝑂 ) } = { 𝑋 } )
156 154 155 eqtr3d ⊢ ( 𝜑 → ( 𝑂 “ { ∪ dom 𝑂 } ) = { 𝑋 } )
157 150 156 difeq12d ⊢ ( 𝜑 → ( ( 𝑂 “ dom 𝑂 ) ∖ ( 𝑂 “ { ∪ dom 𝑂 } ) ) = ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) )
158 ordirr ⊢ ( Ord ∪ dom 𝑂 → ¬ ∪ dom 𝑂 ∈ ∪ dom 𝑂 )
159 144 158 syl ⊢ ( 𝜑 → ¬ ∪ dom 𝑂 ∈ ∪ dom 𝑂 )
160 disjsn ⊢ ( ( ∪ dom 𝑂 ∩ { ∪ dom 𝑂 } ) = ∅ ↔ ¬ ∪ dom 𝑂 ∈ ∪ dom 𝑂 )
161 159 160 sylibr ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∩ { ∪ dom 𝑂 } ) = ∅ )
162 disj3 ⊢ ( ( ∪ dom 𝑂 ∩ { ∪ dom 𝑂 } ) = ∅ ↔ ∪ dom 𝑂 = ( ∪ dom 𝑂 ∖ { ∪ dom 𝑂 } ) )
163 161 162 sylib ⊢ ( 𝜑 → ∪ dom 𝑂 = ( ∪ dom 𝑂 ∖ { ∪ dom 𝑂 } ) )
164 difun2 ⊢ ( ( ∪ dom 𝑂 ∪ { ∪ dom 𝑂 } ) ∖ { ∪ dom 𝑂 } ) = ( ∪ dom 𝑂 ∖ { ∪ dom 𝑂 } )
165 163 164 eqtr4di ⊢ ( 𝜑 → ∪ dom 𝑂 = ( ( ∪ dom 𝑂 ∪ { ∪ dom 𝑂 } ) ∖ { ∪ dom 𝑂 } ) )
166 df-suc ⊢ suc ∪ dom 𝑂 = ( ∪ dom 𝑂 ∪ { ∪ dom 𝑂 } )
167 16 166 eqtrdi ⊢ ( 𝜑 → dom 𝑂 = ( ∪ dom 𝑂 ∪ { ∪ dom 𝑂 } ) )
168 167 difeq1d ⊢ ( 𝜑 → ( dom 𝑂 ∖ { ∪ dom 𝑂 } ) = ( ( ∪ dom 𝑂 ∪ { ∪ dom 𝑂 } ) ∖ { ∪ dom 𝑂 } ) )
169 165 168 eqtr4d ⊢ ( 𝜑 → ∪ dom 𝑂 = ( dom 𝑂 ∖ { ∪ dom 𝑂 } ) )
170 169 imaeq2d ⊢ ( 𝜑 → ( 𝑂 “ ∪ dom 𝑂 ) = ( 𝑂 “ ( dom 𝑂 ∖ { ∪ dom 𝑂 } ) ) )
171 dff1o3 ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) ↔ ( 𝑂 : dom 𝑂 –onto→ ( 𝐹 supp ∅ ) ∧ Fun ◡ 𝑂 ) )
172 171 simprbi ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐹 supp ∅ ) → Fun ◡ 𝑂 )
173 imadif ⊢ ( Fun ◡ 𝑂 → ( 𝑂 “ ( dom 𝑂 ∖ { ∪ dom 𝑂 } ) ) = ( ( 𝑂 “ dom 𝑂 ) ∖ ( 𝑂 “ { ∪ dom 𝑂 } ) ) )
174 30 172 173 3syl ⊢ ( 𝜑 → ( 𝑂 “ ( dom 𝑂 ∖ { ∪ dom 𝑂 } ) ) = ( ( 𝑂 “ dom 𝑂 ) ∖ ( 𝑂 “ { ∪ dom 𝑂 } ) ) )
175 170 174 eqtrd ⊢ ( 𝜑 → ( 𝑂 “ ∪ dom 𝑂 ) = ( ( 𝑂 “ dom 𝑂 ) ∖ ( 𝑂 “ { ∪ dom 𝑂 } ) ) )
176 7 99 ssneldd ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝐺 supp ∅ ) )
177 disjsn ⊢ ( ( ( 𝐺 supp ∅ ) ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ ( 𝐺 supp ∅ ) )
178 176 177 sylibr ⊢ ( 𝜑 → ( ( 𝐺 supp ∅ ) ∩ { 𝑋 } ) = ∅ )
179 fvex ⊢ ( 𝐺 ‘ 𝑋 ) ∈ V
180 dif1o ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ V ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) )
181 179 180 mpbiran ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ↔ ( 𝐺 ‘ 𝑋 ) ≠ ∅ )
182 41 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
183 elsuppfn ⊢ ( ( 𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
184 182 3 47 183 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ) )
185 181 a1i ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ↔ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) )
186 185 bicomd ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ ↔ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) )
187 186 anbi2d ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) ) )
188 184 187 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) ↔ ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) ) )
189 7 sseld ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐺 supp ∅ ) → 𝑋 ∈ 𝑋 ) )
190 188 189 sylbird ⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) ) → 𝑋 ∈ 𝑋 ) )
191 5 190 mpand ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ∈ ( V ∖ 1o ) → 𝑋 ∈ 𝑋 ) )
192 181 191 biimtrrid ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ≠ ∅ → 𝑋 ∈ 𝑋 ) )
193 192 necon1bd ⊢ ( 𝜑 → ( ¬ 𝑋 ∈ 𝑋 → ( 𝐺 ‘ 𝑋 ) = ∅ ) )
194 99 193 mpd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ∅ )
195 194 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝐺 ‘ 𝑋 ) = ∅ )
196 fveqeq2 ⊢ ( 𝑘 = 𝑋 → ( ( 𝐺 ‘ 𝑘 ) = ∅ ↔ ( 𝐺 ‘ 𝑋 ) = ∅ ) )
197 195 196 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝑘 = 𝑋 → ( 𝐺 ‘ 𝑘 ) = ∅ ) )
198 eldifi ⊢ ( 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) → 𝑘 ∈ 𝐵 )
199 198 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → 𝑘 ∈ 𝐵 )
200 6 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → 𝑌 ∈ 𝐴 )
201 200 110 111 sylancl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) ∈ V )
202 8 106 199 201 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝐹 ‘ 𝑘 ) = if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) )
203 ssidd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ( 𝐹 supp ∅ ) )
204 44 203 3 9 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝐹 ‘ 𝑘 ) = ∅ )
205 202 204 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) = ∅ )
206 iffalse ⊢ ( ¬ 𝑘 = 𝑋 → if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
207 206 eqeq1d ⊢ ( ¬ 𝑘 = 𝑋 → ( if ( 𝑘 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑘 ) ) = ∅ ↔ ( 𝐺 ‘ 𝑘 ) = ∅ ) )
208 205 207 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( ¬ 𝑘 = 𝑋 → ( 𝐺 ‘ 𝑘 ) = ∅ ) )
209 197 208 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝐺 ‘ 𝑘 ) = ∅ )
210 41 209 suppss ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ ( 𝐹 supp ∅ ) )
211 reldisj ⊢ ( ( 𝐺 supp ∅ ) ⊆ ( 𝐹 supp ∅ ) → ( ( ( 𝐺 supp ∅ ) ∩ { 𝑋 } ) = ∅ ↔ ( 𝐺 supp ∅ ) ⊆ ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) ) )
212 210 211 syl ⊢ ( 𝜑 → ( ( ( 𝐺 supp ∅ ) ∩ { 𝑋 } ) = ∅ ↔ ( 𝐺 supp ∅ ) ⊆ ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) ) )
213 178 212 mpbid ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) )
214 uncom ⊢ ( ( 𝐺 supp ∅ ) ∪ { 𝑋 } ) = ( { 𝑋 } ∪ ( 𝐺 supp ∅ ) )
215 129 214 sseqtrdi ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ( { 𝑋 } ∪ ( 𝐺 supp ∅ ) ) )
216 ssundif ⊢ ( ( 𝐹 supp ∅ ) ⊆ ( { 𝑋 } ∪ ( 𝐺 supp ∅ ) ) ↔ ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) ⊆ ( 𝐺 supp ∅ ) )
217 215 216 sylib ⊢ ( 𝜑 → ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) ⊆ ( 𝐺 supp ∅ ) )
218 213 217 eqssd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) = ( ( 𝐹 supp ∅ ) ∖ { 𝑋 } ) )
219 157 175 218 3eqtr4rd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) = ( 𝑂 “ ∪ dom 𝑂 ) )
220 isores3 ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐹 supp ∅ ) ) ∧ ∪ dom 𝑂 ⊆ dom 𝑂 ∧ ( 𝐺 supp ∅ ) = ( 𝑂 “ ∪ dom 𝑂 ) ) → ( 𝑂 ↾ ∪ dom 𝑂 ) Isom E , E ( ∪ dom 𝑂 , ( 𝐺 supp ∅ ) ) )
221 28 146 219 220 syl3anc ⊢ ( 𝜑 → ( 𝑂 ↾ ∪ dom 𝑂 ) Isom E , E ( ∪ dom 𝑂 , ( 𝐺 supp ∅ ) ) )
222 1 2 3 12 4 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐺 supp ∅ ) ∧ dom 𝐾 ∈ ω ) )
223 222 simpld ⊢ ( 𝜑 → E We ( 𝐺 supp ∅ ) )
224 epse ⊢ E Se ( 𝐺 supp ∅ )
225 12 oieu ⊢ ( ( E We ( 𝐺 supp ∅ ) ∧ E Se ( 𝐺 supp ∅ ) ) → ( ( Ord ∪ dom 𝑂 ∧ ( 𝑂 ↾ ∪ dom 𝑂 ) Isom E , E ( ∪ dom 𝑂 , ( 𝐺 supp ∅ ) ) ) ↔ ( ∪ dom 𝑂 = dom 𝐾 ∧ ( 𝑂 ↾ ∪ dom 𝑂 ) = 𝐾 ) ) )
226 223 224 225 sylancl ⊢ ( 𝜑 → ( ( Ord ∪ dom 𝑂 ∧ ( 𝑂 ↾ ∪ dom 𝑂 ) Isom E , E ( ∪ dom 𝑂 , ( 𝐺 supp ∅ ) ) ) ↔ ( ∪ dom 𝑂 = dom 𝐾 ∧ ( 𝑂 ↾ ∪ dom 𝑂 ) = 𝐾 ) ) )
227 144 221 226 mpbi2and ⊢ ( 𝜑 → ( ∪ dom 𝑂 = dom 𝐾 ∧ ( 𝑂 ↾ ∪ dom 𝑂 ) = 𝐾 ) )
228 227 simpld ⊢ ( 𝜑 → ∪ dom 𝑂 = dom 𝐾 )
229 228 fveq2d ⊢ ( 𝜑 → ( 𝑀 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ dom 𝐾 ) )
230 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂 ) )
231 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ∅ ) )
232 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∅ ) )
233 13 seqom0g ⊢ ( ∅ ∈ V → ( 𝑀 ‘ ∅ ) = ∅ )
234 46 233 ax-mp ⊢ ( 𝑀 ‘ ∅ ) = ∅
235 232 234 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑀 ‘ 𝑥 ) = ∅ )
236 231 235 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ↔ ( 𝐻 ‘ ∅ ) = ∅ ) )
237 230 236 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ↔ ( ∅ ∈ dom 𝑂 → ( 𝐻 ‘ ∅ ) = ∅ ) ) )
238 237 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝜑 → ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ∅ ∈ dom 𝑂 → ( 𝐻 ‘ ∅ ) = ∅ ) ) ) )
239 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ dom 𝑂 ↔ 𝑦 ∈ dom 𝑂 ) )
240 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑦 ) )
241 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑦 ) )
242 240 241 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ↔ ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) )
243 239 242 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ↔ ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) ) )
244 243 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) ) ) )
245 eleq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂 ) )
246 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ suc 𝑦 ) )
247 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ suc 𝑦 ) )
248 246 247 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ↔ ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) )
249 245 248 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ↔ ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) )
250 249 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝜑 → ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) ) )
251 eleq1 ⊢ ( 𝑥 = ∪ dom 𝑂 → ( 𝑥 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂 ) )
252 fveq2 ⊢ ( 𝑥 = ∪ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ ∪ dom 𝑂 ) )
253 fveq2 ⊢ ( 𝑥 = ∪ dom 𝑂 → ( 𝑀 ‘ 𝑥 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) )
254 252 253 eqeq12d ⊢ ( 𝑥 = ∪ dom 𝑂 → ( ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ↔ ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) ) )
255 251 254 imbi12d ⊢ ( 𝑥 = ∪ dom 𝑂 → ( ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ↔ ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) ) ) )
256 255 imbi2d ⊢ ( 𝑥 = ∪ dom 𝑂 → ( ( 𝜑 → ( 𝑥 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) ) ) ↔ ( 𝜑 → ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) ) ) ) )
257 11 seqom0g ⊢ ( ∅ ∈ dom 𝑂 → ( 𝐻 ‘ ∅ ) = ∅ )
258 257 a1i ⊢ ( 𝜑 → ( ∅ ∈ dom 𝑂 → ( 𝐻 ‘ ∅ ) = ∅ ) )
259 nnord ⊢ ( dom 𝑂 ∈ ω → Ord dom 𝑂 )
260 19 259 syl ⊢ ( 𝜑 → Ord dom 𝑂 )
261 ordtr ⊢ ( Ord dom 𝑂 → Tr dom 𝑂 )
262 260 261 syl ⊢ ( 𝜑 → Tr dom 𝑂 )
263 trsuc ⊢ ( ( Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ dom 𝑂 )
264 262 263 sylan ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ dom 𝑂 )
265 264 ex ⊢ ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 → 𝑦 ∈ dom 𝑂 ) )
266 265 imim1d ⊢ ( 𝜑 → ( ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) ) )
267 oveq2 ⊢ ( ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) → ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) )
268 elnn ⊢ ( ( 𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω ) → 𝑦 ∈ ω )
269 268 ancoms ⊢ ( ( dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ ω )
270 19 264 269 syl2an2r ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ ω )
271 1 2 3 10 14 11 cantnfsuc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( 𝐻 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
272 270 271 syldan ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐻 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) )
273 1 2 3 12 4 13 cantnfsuc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ω ) → ( 𝑀 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑦 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) )
274 270 273 syldan ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝑀 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑦 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) )
275 227 simprd ⊢ ( 𝜑 → ( 𝑂 ↾ ∪ dom 𝑂 ) = 𝐾 )
276 275 fveq1d ⊢ ( 𝜑 → ( ( 𝑂 ↾ ∪ dom 𝑂 ) ‘ 𝑦 ) = ( 𝐾 ‘ 𝑦 ) )
277 276 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( 𝑂 ↾ ∪ dom 𝑂 ) ‘ 𝑦 ) = ( 𝐾 ‘ 𝑦 ) )
278 16 eleq2d ⊢ ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂 ) )
279 278 biimpa ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → suc 𝑦 ∈ suc ∪ dom 𝑂 )
280 144 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → Ord ∪ dom 𝑂 )
281 ordsucelsuc ⊢ ( Ord ∪ dom 𝑂 → ( 𝑦 ∈ ∪ dom 𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂 ) )
282 280 281 syl ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝑦 ∈ ∪ dom 𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂 ) )
283 279 282 mpbird ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ ∪ dom 𝑂 )
284 283 fvresd ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( 𝑂 ↾ ∪ dom 𝑂 ) ‘ 𝑦 ) = ( 𝑂 ‘ 𝑦 ) )
285 277 284 eqtr3d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐾 ‘ 𝑦 ) = ( 𝑂 ‘ 𝑦 ) )
286 285 oveq2d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐴 ↑o ( 𝐾 ‘ 𝑦 ) ) = ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) )
287 eqeq1 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑦 ) → ( 𝑡 = 𝑋 ↔ ( 𝐾 ‘ 𝑦 ) = 𝑋 ) )
288 fveq2 ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑦 ) → ( 𝐺 ‘ 𝑡 ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) )
289 287 288 ifbieq2d ⊢ ( 𝑡 = ( 𝐾 ‘ 𝑦 ) → if ( 𝑡 = 𝑋 , 𝑌 , ( 𝐺 ‘ 𝑡 ) ) = if ( ( 𝐾 ‘ 𝑦 ) = 𝑋 , 𝑌 , ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) )
290 suppssdm ⊢ ( 𝐺 supp ∅ ) ⊆ dom 𝐺
291 290 41 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
292 291 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
293 228 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ∪ dom 𝑂 = dom 𝐾 )
294 283 293 eleqtrd ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑦 ∈ dom 𝐾 )
295 12 oif ⊢ 𝐾 : dom 𝐾 ⟶ ( 𝐺 supp ∅ )
296 295 ffvelcdmi ⊢ ( 𝑦 ∈ dom 𝐾 → ( 𝐾 ‘ 𝑦 ) ∈ ( 𝐺 supp ∅ ) )
297 294 296 syl ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐾 ‘ 𝑦 ) ∈ ( 𝐺 supp ∅ ) )
298 292 297 sseldd ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐾 ‘ 𝑦 ) ∈ 𝐵 )
299 6 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → 𝑌 ∈ 𝐴 )
300 fvex ⊢ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ∈ V
301 ifexg ⊢ ( ( 𝑌 ∈ 𝐴 ∧ ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ∈ V ) → if ( ( 𝐾 ‘ 𝑦 ) = 𝑋 , 𝑌 , ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ∈ V )
302 299 300 301 sylancl ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → if ( ( 𝐾 ‘ 𝑦 ) = 𝑋 , 𝑌 , ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) ∈ V )
303 8 289 298 302 fvmptd3 ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑦 ) ) = if ( ( 𝐾 ‘ 𝑦 ) = 𝑋 , 𝑌 , ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) )
304 285 fveq2d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐹 ‘ ( 𝐾 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) )
305 176 adantr ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ¬ 𝑋 ∈ ( 𝐺 supp ∅ ) )
306 nelneq ⊢ ( ( ( 𝐾 ‘ 𝑦 ) ∈ ( 𝐺 supp ∅ ) ∧ ¬ 𝑋 ∈ ( 𝐺 supp ∅ ) ) → ¬ ( 𝐾 ‘ 𝑦 ) = 𝑋 )
307 297 305 306 syl2anc ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ¬ ( 𝐾 ‘ 𝑦 ) = 𝑋 )
308 307 iffalsed ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → if ( ( 𝐾 ‘ 𝑦 ) = 𝑋 , 𝑌 , ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) = ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) )
309 303 304 308 3eqtr3rd ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) = ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) )
310 286 309 oveq12d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑦 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) = ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) )
311 310 oveq1d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( ( 𝐴 ↑o ( 𝐾 ‘ 𝑦 ) ) ·o ( 𝐺 ‘ ( 𝐾 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) )
312 274 311 eqtrd ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( 𝑀 ‘ suc 𝑦 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) )
313 272 312 eqeq12d ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ↔ ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝐻 ‘ 𝑦 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ 𝑦 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ 𝑦 ) ) ) +o ( 𝑀 ‘ 𝑦 ) ) ) )
314 267 313 imbitrrid ⊢ ( ( 𝜑 ∧ suc 𝑦 ∈ dom 𝑂 ) → ( ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) )
315 314 ex ⊢ ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 → ( ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) )
316 315 a2d ⊢ ( 𝜑 → ( ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) )
317 266 316 syld ⊢ ( 𝜑 → ( ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) )
318 317 a2i ⊢ ( ( 𝜑 → ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) ) → ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) )
319 318 a1i ⊢ ( 𝑦 ∈ ω → ( ( 𝜑 → ( 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) ) ) → ( 𝜑 → ( suc 𝑦 ∈ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝑀 ‘ suc 𝑦 ) ) ) ) )
320 238 244 250 256 258 319 finds ⊢ ( ∪ dom 𝑂 ∈ ω → ( 𝜑 → ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) ) ) )
321 22 320 mpcom ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) ) )
322 64 321 mpd ⊢ ( 𝜑 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( 𝑀 ‘ ∪ dom 𝑂 ) )
323 1 2 3 12 4 13 cantnfval ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = ( 𝑀 ‘ dom 𝐾 ) )
324 229 322 323 3eqtr4d ⊢ ( 𝜑 → ( 𝐻 ‘ ∪ dom 𝑂 ) = ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )
325 142 324 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 ↑o ( 𝑂 ‘ ∪ dom 𝑂 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ ∪ dom 𝑂 ) ) ) +o ( 𝐻 ‘ ∪ dom 𝑂 ) ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
326 24 325 eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ suc ∪ dom 𝑂 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )
327 15 17 326 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( ( 𝐴 ↑o 𝑋 ) ·o 𝑌 ) +o ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) ) )