Metamath Proof Explorer

Theorem cantnflem1

Description: Lemma for cantnf . This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation T is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct F , G are T -related as F < G or G < F , and WLOG assuming that F < G , we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-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 cantnflem1 ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )

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 ovex ⊢ ( 𝐺 supp ∅ ) ∈ V
12 9 oion ⊢ ( ( 𝐺 supp ∅ ) ∈ V → dom 𝑂 ∈ On )
13 11 12 mp1i ⊢ ( 𝜑 → dom 𝑂 ∈ On )
14 uniexg ⊢ ( dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V )
15 sucidg ⊢ ( ∪ dom 𝑂 ∈ V → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂 )
16 13 14 15 3syl ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂 )
17 1 2 3 4 5 6 7 8 cantnflem1a ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐺 supp ∅ ) )
18 n0i ⊢ ( 𝑋 ∈ ( 𝐺 supp ∅ ) → ¬ ( 𝐺 supp ∅ ) = ∅ )
19 17 18 syl ⊢ ( 𝜑 → ¬ ( 𝐺 supp ∅ ) = ∅ )
20 ovexd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ∈ V )
21 1 2 3 9 6 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐺 supp ∅ ) ∧ dom 𝑂 ∈ ω ) )
22 21 simpld ⊢ ( 𝜑 → E We ( 𝐺 supp ∅ ) )
23 9 oien ⊢ ( ( ( 𝐺 supp ∅ ) ∈ V ∧ E We ( 𝐺 supp ∅ ) ) → dom 𝑂 ≈ ( 𝐺 supp ∅ ) )
24 20 22 23 syl2anc ⊢ ( 𝜑 → dom 𝑂 ≈ ( 𝐺 supp ∅ ) )
25 breq1 ⊢ ( dom 𝑂 = ∅ → ( dom 𝑂 ≈ ( 𝐺 supp ∅ ) ↔ ∅ ≈ ( 𝐺 supp ∅ ) ) )
26 ensymb ⊢ ( ∅ ≈ ( 𝐺 supp ∅ ) ↔ ( 𝐺 supp ∅ ) ≈ ∅ )
27 en0 ⊢ ( ( 𝐺 supp ∅ ) ≈ ∅ ↔ ( 𝐺 supp ∅ ) = ∅ )
28 26 27 bitri ⊢ ( ∅ ≈ ( 𝐺 supp ∅ ) ↔ ( 𝐺 supp ∅ ) = ∅ )
29 25 28 bitrdi ⊢ ( dom 𝑂 = ∅ → ( dom 𝑂 ≈ ( 𝐺 supp ∅ ) ↔ ( 𝐺 supp ∅ ) = ∅ ) )
30 24 29 syl5ibcom ⊢ ( 𝜑 → ( dom 𝑂 = ∅ → ( 𝐺 supp ∅ ) = ∅ ) )
31 19 30 mtod ⊢ ( 𝜑 → ¬ dom 𝑂 = ∅ )
32 21 simprd ⊢ ( 𝜑 → dom 𝑂 ∈ ω )
33 nnlim ⊢ ( dom 𝑂 ∈ ω → ¬ Lim dom 𝑂 )
34 32 33 syl ⊢ ( 𝜑 → ¬ Lim dom 𝑂 )
35 ioran ⊢ ( ¬ ( dom 𝑂 = ∅ ∨ Lim dom 𝑂 ) ↔ ( ¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂 ) )
36 31 34 35 sylanbrc ⊢ ( 𝜑 → ¬ ( dom 𝑂 = ∅ ∨ Lim dom 𝑂 ) )
37 9 oicl ⊢ Ord dom 𝑂
38 unizlim ⊢ ( Ord dom 𝑂 → ( dom 𝑂 = ∪ dom 𝑂 ↔ ( dom 𝑂 = ∅ ∨ Lim dom 𝑂 ) ) )
39 37 38 mp1i ⊢ ( 𝜑 → ( dom 𝑂 = ∪ dom 𝑂 ↔ ( dom 𝑂 = ∅ ∨ Lim dom 𝑂 ) ) )
40 36 39 mtbird ⊢ ( 𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂 )
41 orduniorsuc ⊢ ( Ord dom 𝑂 → ( dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂 ) )
42 37 41 mp1i ⊢ ( 𝜑 → ( dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂 ) )
43 42 ord ⊢ ( 𝜑 → ( ¬ dom 𝑂 = ∪ dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂 ) )
44 40 43 mpd ⊢ ( 𝜑 → dom 𝑂 = suc ∪ dom 𝑂 )
45 16 44 eleqtrrd ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ dom 𝑂 )
46 9 oiiso ⊢ ( ( ( 𝐺 supp ∅ ) ∈ V ∧ E We ( 𝐺 supp ∅ ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
47 20 22 46 syl2anc ⊢ ( 𝜑 → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
48 isof1o ⊢ ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
49 47 48 syl ⊢ ( 𝜑 → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
50 f1ocnv ⊢ ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) → ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 )
51 f1of ⊢ ( ◡ 𝑂 : ( 𝐺 supp ∅ ) –1-1-onto→ dom 𝑂 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
52 49 50 51 3syl ⊢ ( 𝜑 → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
53 52 17 ffvelcdmd ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
54 elssuni ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 )
55 53 54 syl ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 )
56 44 32 eqeltrrd ⊢ ( 𝜑 → suc ∪ dom 𝑂 ∈ ω )
57 peano2b ⊢ ( ∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω )
58 56 57 sylibr ⊢ ( 𝜑 → ∪ dom 𝑂 ∈ ω )
59 eleq1 ⊢ ( 𝑦 = ∪ dom 𝑂 → ( 𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂 ) )
60 sseq2 ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) )
61 59 60 anbi12d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) ↔ ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) ) )
62 fveq2 ⊢ ( 𝑦 = ∪ dom 𝑂 → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ ∪ dom 𝑂 ) )
63 62 sseq2d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
64 63 ifbid ⊢ ( 𝑦 = ∪ dom 𝑂 → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
65 64 mpteq2dv ⊢ ( 𝑦 = ∪ dom 𝑂 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
66 65 fveq2d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
67 suceq ⊢ ( 𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂 )
68 67 fveq2d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝐻 ‘ suc ∪ dom 𝑂 ) )
69 66 68 eleq12d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) ) )
70 61 69 imbi12d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ↔ ( ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) ) ) )
71 70 imbi2d ⊢ ( 𝑦 = ∪ dom 𝑂 → ( ( 𝜑 → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ) ↔ ( 𝜑 → ( ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) ) ) ) )
72 eleq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂 ) )
73 sseq2 ⊢ ( 𝑦 = ∅ → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ ) )
74 72 73 anbi12d ⊢ ( 𝑦 = ∅ → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) ↔ ( ∅ ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ ) ) )
75 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ ∅ ) )
76 75 sseq2d ⊢ ( 𝑦 = ∅ → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( 𝑂 ‘ ∅ ) ) )
77 76 ifbid ⊢ ( 𝑦 = ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
78 77 mpteq2dv ⊢ ( 𝑦 = ∅ → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
79 78 fveq2d ⊢ ( 𝑦 = ∅ → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
80 suceq ⊢ ( 𝑦 = ∅ → suc 𝑦 = suc ∅ )
81 80 fveq2d ⊢ ( 𝑦 = ∅ → ( 𝐻 ‘ suc 𝑦 ) = ( 𝐻 ‘ suc ∅ ) )
82 79 81 eleq12d ⊢ ( 𝑦 = ∅ → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∅ ) ) )
83 74 82 imbi12d ⊢ ( 𝑦 = ∅ → ( ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ↔ ( ( ∅ ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∅ ) ) ) )
84 eleq1 ⊢ ( 𝑦 = 𝑢 → ( 𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂 ) )
85 sseq2 ⊢ ( 𝑦 = 𝑢 → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) )
86 84 85 anbi12d ⊢ ( 𝑦 = 𝑢 → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) ↔ ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) )
87 fveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ 𝑢 ) )
88 87 sseq2d ⊢ ( 𝑦 = 𝑢 → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) )
89 88 ifbid ⊢ ( 𝑦 = 𝑢 → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
90 89 mpteq2dv ⊢ ( 𝑦 = 𝑢 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
91 90 fveq2d ⊢ ( 𝑦 = 𝑢 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
92 suceq ⊢ ( 𝑦 = 𝑢 → suc 𝑦 = suc 𝑢 )
93 92 fveq2d ⊢ ( 𝑦 = 𝑢 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝐻 ‘ suc 𝑢 ) )
94 91 93 eleq12d ⊢ ( 𝑦 = 𝑢 → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) )
95 86 94 imbi12d ⊢ ( 𝑦 = 𝑢 → ( ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ↔ ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) ) )
96 eleq1 ⊢ ( 𝑦 = suc 𝑢 → ( 𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂 ) )
97 sseq2 ⊢ ( 𝑦 = suc 𝑢 → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) )
98 96 97 anbi12d ⊢ ( 𝑦 = suc 𝑢 → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) ↔ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) ) )
99 fveq2 ⊢ ( 𝑦 = suc 𝑢 → ( 𝑂 ‘ 𝑦 ) = ( 𝑂 ‘ suc 𝑢 ) )
100 99 sseq2d ⊢ ( 𝑦 = suc 𝑢 → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ) )
101 100 ifbid ⊢ ( 𝑦 = suc 𝑢 → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
102 101 mpteq2dv ⊢ ( 𝑦 = suc 𝑢 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
103 102 fveq2d ⊢ ( 𝑦 = suc 𝑢 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
104 suceq ⊢ ( 𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢 )
105 104 fveq2d ⊢ ( 𝑦 = suc 𝑢 → ( 𝐻 ‘ suc 𝑦 ) = ( 𝐻 ‘ suc suc 𝑢 ) )
106 103 105 eleq12d ⊢ ( 𝑦 = suc 𝑢 → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
107 98 106 imbi12d ⊢ ( 𝑦 = suc 𝑢 → ( ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ↔ ( ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
108 f1ocnvfv2 ⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) ∧ 𝑋 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
109 49 17 108 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
110 109 sseq2d ⊢ ( 𝜑 → ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ 𝑥 ⊆ 𝑋 ) )
111 110 ifbid ⊢ ( 𝜑 → if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
112 111 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
113 112 fveq2d ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
114 1 2 3 4 5 6 7 8 9 10 cantnflem1d ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ 𝑋 , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) )
115 113 114 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) )
116 ss0 ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( ◡ 𝑂 ‘ 𝑋 ) = ∅ )
117 116 fveq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = ( 𝑂 ‘ ∅ ) )
118 117 sseq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ 𝑥 ⊆ ( 𝑂 ‘ ∅ ) ) )
119 118 ifbid ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
120 119 mpteq2dv ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
121 120 fveq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
122 suceq ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = ∅ → suc ( ◡ 𝑂 ‘ 𝑋 ) = suc ∅ )
123 116 122 syl ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → suc ( ◡ 𝑂 ‘ 𝑋 ) = suc ∅ )
124 123 fveq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) = ( 𝐻 ‘ suc ∅ ) )
125 121 124 eleq12d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∅ ) ) )
126 125 adantl ⊢ ( ( ∅ ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∅ ) ) )
127 115 126 syl5ibcom ⊢ ( 𝜑 → ( ( ∅ ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∅ ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∅ ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∅ ) ) )
128 ordelon ⊢ ( ( Ord dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
129 37 53 128 sylancr ⊢ ( 𝜑 → ( ◡ 𝑂 ‘ 𝑋 ) ∈ On )
130 37 a1i ⊢ ( 𝜑 → Ord dom 𝑂 )
131 ordelon ⊢ ( ( Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) → suc 𝑢 ∈ On )
132 130 131 sylan ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → suc 𝑢 ∈ On )
133 onsseleq ⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On ∧ suc 𝑢 ∈ On ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ↔ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ∨ ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 ) ) )
134 129 132 133 syl2an2r ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ↔ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ∨ ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 ) ) )
135 onsucb ⊢ ( 𝑢 ∈ On ↔ suc 𝑢 ∈ On )
136 132 135 sylibr ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → 𝑢 ∈ On )
137 eloni ⊢ ( 𝑢 ∈ On → Ord 𝑢 )
138 136 137 syl ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → Ord 𝑢 )
139 ordsssuc ⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On ∧ Ord 𝑢 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ) )
140 129 138 139 syl2an2r ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ) )
141 ordtr ⊢ ( Ord dom 𝑂 → Tr dom 𝑂 )
142 37 141 mp1i ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → Tr dom 𝑂 )
143 simprl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → suc 𝑢 ∈ dom 𝑂 )
144 trsuc ⊢ ( ( Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) → 𝑢 ∈ dom 𝑂 )
145 142 143 144 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑢 ∈ dom 𝑂 )
146 simprr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 )
147 145 146 jca ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) )
148 3 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝐵 ∈ On )
149 oecl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
150 2 148 149 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐴 ↑o 𝐵 ) ∈ On )
151 2 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝐴 ∈ On )
152 1 151 148 cantnff ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐴 CNF 𝐵 ) : 𝑆 ⟶ ( 𝐴 ↑o 𝐵 ) )
153 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
154 5 153 mpbid ⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) )
155 154 simpld ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
156 155 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐴 )
157 1 2 3 cantnfs ⊢ ( 𝜑 → ( 𝐺 ∈ 𝑆 ↔ ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) ) )
158 6 157 mpbid ⊢ ( 𝜑 → ( 𝐺 : 𝐵 ⟶ 𝐴 ∧ 𝐺 finSupp ∅ ) )
159 158 simpld ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
160 1 2 3 4 5 6 7 8 oemapvali ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( 𝐺 ‘ 𝑋 ) ∧ ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ) )
161 160 simp1d ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
162 159 161 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
163 162 ne0d ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
164 on0eln0 ⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
165 2 164 syl ⊢ ( 𝜑 → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
166 163 165 mpbird ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
167 166 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∅ ∈ 𝐴 )
168 156 167 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ 𝐴 )
169 168 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) : 𝐵 ⟶ 𝐴 )
170 3 mptexd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ V )
171 funmpt ⊢ Fun ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
172 171 a1i ⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
173 154 simprd ⊢ ( 𝜑 → 𝐹 finSupp ∅ )
174 ssidd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ( 𝐹 supp ∅ ) )
175 0ex ⊢ ∅ ∈ V
176 175 a1i ⊢ ( 𝜑 → ∅ ∈ V )
177 155 174 3 176 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
178 177 ifeq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ∅ , ∅ ) )
179 ifid ⊢ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ∅ , ∅ ) = ∅
180 178 179 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ( 𝐹 supp ∅ ) ) ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = ∅ )
181 180 3 suppss2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) ⊆ ( 𝐹 supp ∅ ) )
182 fsuppsssupp ⊢ ( ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∧ ( 𝐹 finSupp ∅ ∧ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) ⊆ ( 𝐹 supp ∅ ) ) ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) finSupp ∅ )
183 170 172 173 181 182 syl22anc ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) finSupp ∅ )
184 1 2 3 cantnfs ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ 𝑆 ↔ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) : 𝐵 ⟶ 𝐴 ∧ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) finSupp ∅ ) ) )
185 169 183 184 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ 𝑆 )
186 185 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ 𝑆 )
187 152 186 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝐵 ) )
188 onelon ⊢ ( ( ( 𝐴 ↑o 𝐵 ) ∈ On ∧ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐴 ↑o 𝐵 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ On )
189 150 187 188 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ On )
190 32 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → dom 𝑂 ∈ ω )
191 elnn ⊢ ( ( suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω ) → suc 𝑢 ∈ ω )
192 143 190 191 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → suc 𝑢 ∈ ω )
193 10 cantnfvalf ⊢ 𝐻 : ω ⟶ On
194 193 ffvelcdmi ⊢ ( suc 𝑢 ∈ ω → ( 𝐻 ‘ suc 𝑢 ) ∈ On )
195 192 194 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐻 ‘ suc 𝑢 ) ∈ On )
196 suppssdm ⊢ ( 𝐺 supp ∅ ) ⊆ dom 𝐺
197 196 159 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
198 197 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐺 supp ∅ ) ⊆ 𝐵 )
199 9 oif ⊢ 𝑂 : dom 𝑂 ⟶ ( 𝐺 supp ∅ )
200 199 ffvelcdmi ⊢ ( suc 𝑢 ∈ dom 𝑂 → ( 𝑂 ‘ suc 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
201 143 200 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ suc 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
202 198 201 sseldd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ suc 𝑢 ) ∈ 𝐵 )
203 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑂 ‘ suc 𝑢 ) ∈ 𝐵 ) → ( 𝑂 ‘ suc 𝑢 ) ∈ On )
204 3 202 203 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ suc 𝑢 ) ∈ On )
205 oecl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑂 ‘ suc 𝑢 ) ∈ On ) → ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ∈ On )
206 2 204 205 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ∈ On )
207 155 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝐹 : 𝐵 ⟶ 𝐴 )
208 207 202 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ∈ 𝐴 )
209 onelon ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ∈ On )
210 2 208 209 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ∈ On )
211 omcl ⊢ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ∈ On ∧ ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ∈ On ) → ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) ∈ On )
212 206 210 211 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) ∈ On )
213 oaord ⊢ ( ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ On ∧ ( 𝐻 ‘ suc 𝑢 ) ∈ On ∧ ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) ∈ On ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ↔ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) ) )
214 189 195 212 213 syl3anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ↔ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) ) )
215 ifeq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ∅ , ∅ ) )
216 ifid ⊢ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ∅ , ∅ ) = ∅
217 215 216 eqtrdi ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = ∅ )
218 ifeq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ∅ , ∅ ) )
219 ifid ⊢ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ∅ , ∅ ) = ∅
220 218 219 eqtrdi ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = ∅ )
221 217 220 eqeq12d ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → ( if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ↔ ∅ = ∅ ) )
222 onss ⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
223 3 222 syl ⊢ ( 𝜑 → 𝐵 ⊆ On )
224 223 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
225 224 adantlr ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
226 204 adantr ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ suc 𝑢 ) ∈ On )
227 onsseleq ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑂 ‘ suc 𝑢 ) ∈ On ) → ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ) )
228 225 226 227 syl2anc ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ) )
229 228 adantr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ) )
230 199 ffvelcdmi ⊢ ( 𝑢 ∈ dom 𝑂 → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
231 145 230 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝐺 supp ∅ ) )
232 198 231 sseldd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ 𝐵 )
233 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝐵 ) → ( 𝑂 ‘ 𝑢 ) ∈ On )
234 3 232 233 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ On )
235 234 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑂 ‘ 𝑢 ) ∈ On )
236 onsssuc ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑂 ‘ 𝑢 ) ∈ On ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ 𝑥 ∈ suc ( 𝑂 ‘ 𝑢 ) ) )
237 225 235 236 syl2an2r ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ 𝑥 ∈ suc ( 𝑂 ‘ 𝑢 ) ) )
238 vex ⊢ 𝑢 ∈ V
239 238 sucid ⊢ 𝑢 ∈ suc 𝑢
240 47 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
241 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( 𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) ) → ( 𝑢 E suc 𝑢 ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ suc 𝑢 ) ) )
242 240 145 143 241 syl12anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 E suc 𝑢 ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ suc 𝑢 ) ) )
243 238 sucex ⊢ suc 𝑢 ∈ V
244 243 epeli ⊢ ( 𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢 )
245 fvex ⊢ ( 𝑂 ‘ suc 𝑢 ) ∈ V
246 245 epeli ⊢ ( ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ suc 𝑢 ) )
247 242 244 246 3bitr3g ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑢 ∈ suc 𝑢 ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
248 239 247 mpbii ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ suc 𝑢 ) )
249 eloni ⊢ ( ( 𝑂 ‘ suc 𝑢 ) ∈ On → Ord ( 𝑂 ‘ suc 𝑢 ) )
250 204 249 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → Ord ( 𝑂 ‘ suc 𝑢 ) )
251 ordelsuc ⊢ ( ( ( 𝑂 ‘ 𝑢 ) ∈ On ∧ Ord ( 𝑂 ‘ suc 𝑢 ) ) → ( ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ suc 𝑢 ) ↔ suc ( 𝑂 ‘ 𝑢 ) ⊆ ( 𝑂 ‘ suc 𝑢 ) ) )
252 234 250 251 syl2anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ suc 𝑢 ) ↔ suc ( 𝑂 ‘ 𝑢 ) ⊆ ( 𝑂 ‘ suc 𝑢 ) ) )
253 248 252 mpbid ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → suc ( 𝑂 ‘ 𝑢 ) ⊆ ( 𝑂 ‘ suc 𝑢 ) )
254 253 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → suc ( 𝑂 ‘ 𝑢 ) ⊆ ( 𝑂 ‘ suc 𝑢 ) )
255 254 sseld ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∈ suc ( 𝑂 ‘ 𝑢 ) → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
256 237 255 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
257 simprr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 )
258 240 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
259 258 48 syl ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
260 1 2 3 4 5 6 7 8 9 cantnflem1c ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐺 supp ∅ ) )
261 f1ocnvfv2 ⊢ ( ( 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) = 𝑥 )
262 259 260 261 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) = 𝑥 )
263 257 262 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) )
264 145 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑢 ∈ dom 𝑂 )
265 259 50 51 3syl ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
266 265 260 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 )
267 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 ) ) → ( 𝑢 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
268 258 264 266 267 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑢 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
269 fvex ⊢ ( ◡ 𝑂 ‘ 𝑥 ) ∈ V
270 269 epeli ⊢ ( 𝑢 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) )
271 fvex ⊢ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ∈ V
272 271 epeli ⊢ ( ( 𝑂 ‘ 𝑢 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) )
273 268 270 272 3bitr3g ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ 𝑢 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
274 263 273 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) )
275 ordelon ⊢ ( ( Ord dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ On )
276 37 266 275 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ On )
277 eloni ⊢ ( ( ◡ 𝑂 ‘ 𝑥 ) ∈ On → Ord ( ◡ 𝑂 ‘ 𝑥 ) )
278 276 277 syl ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → Ord ( ◡ 𝑂 ‘ 𝑥 ) )
279 ordelsuc ⊢ ( ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ∧ Ord ( ◡ 𝑂 ‘ 𝑥 ) ) → ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ↔ suc 𝑢 ⊆ ( ◡ 𝑂 ‘ 𝑥 ) ) )
280 274 278 279 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( 𝑢 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ↔ suc 𝑢 ⊆ ( ◡ 𝑂 ‘ 𝑥 ) ) )
281 274 280 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → suc 𝑢 ⊆ ( ◡ 𝑂 ‘ 𝑥 ) )
282 143 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → suc 𝑢 ∈ dom 𝑂 )
283 37 282 131 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → suc 𝑢 ∈ On )
284 ontri1 ⊢ ( ( suc 𝑢 ∈ On ∧ ( ◡ 𝑂 ‘ 𝑥 ) ∈ On ) → ( suc 𝑢 ⊆ ( ◡ 𝑂 ‘ 𝑥 ) ↔ ¬ ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 ) )
285 283 276 284 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( suc 𝑢 ⊆ ( ◡ 𝑂 ‘ 𝑥 ) ↔ ¬ ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 ) )
286 281 285 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ¬ ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 )
287 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) ) → ( ( ◡ 𝑂 ‘ 𝑥 ) E suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) E ( 𝑂 ‘ suc 𝑢 ) ) )
288 258 266 282 287 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ( ◡ 𝑂 ‘ 𝑥 ) E suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) E ( 𝑂 ‘ suc 𝑢 ) ) )
289 243 epeli ⊢ ( ( ◡ 𝑂 ‘ 𝑥 ) E suc 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 )
290 245 epeli ⊢ ( ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) E ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) )
291 288 289 290 3bitr3g ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
292 262 eleq1d ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) ↔ 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
293 291 292 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ( ( ◡ 𝑂 ‘ 𝑥 ) ∈ suc 𝑢 ↔ 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
294 286 293 mtbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) ) → ¬ 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) )
295 294 expr ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 → ¬ 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
296 295 con2d ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) → ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) )
297 ontri1 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑂 ‘ 𝑢 ) ∈ On ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) )
298 225 235 297 syl2an2r ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ ¬ ( 𝑂 ‘ 𝑢 ) ∈ 𝑥 ) )
299 296 298 sylibrd ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) → 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) )
300 256 299 impbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
301 300 orbi1d ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ↔ ( 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ) )
302 229 301 bitr4d ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ) )
303 orcom ⊢ ( ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ∨ 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ) ↔ ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) )
304 302 303 bitrdi ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) ) )
305 304 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑥 ) ≠ ∅ ) → if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
306 eqidd ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ∅ = ∅ )
307 221 305 306 pm2.61ne ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
308 307 mpteq2dva ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
309 308 fveq2d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
310 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
311 310 175 ifex ⊢ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V
312 311 a1i ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V )
313 312 ralrimivw ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V )
314 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
315 314 fnmpt ⊢ ( ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) Fn 𝐵 )
316 313 315 syl ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) Fn 𝐵 )
317 175 a1i ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ∅ ∈ V )
318 suppvalfn ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) = { 𝑦 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ≠ ∅ } )
319 nfcv ⊢ Ⅎ 𝑦 𝐵
320 nfcv ⊢ Ⅎ 𝑥 𝐵
321 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 )
322 nfcv ⊢ Ⅎ 𝑥 ∅
323 321 322 nfne ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ≠ ∅
324 nfv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅
325 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) = ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) )
326 325 neeq1d ⊢ ( 𝑦 = 𝑥 → ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ≠ ∅ ↔ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ ) )
327 319 320 323 324 326 cbvrabw ⊢ { 𝑦 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ≠ ∅ } = { 𝑥 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ }
328 318 327 eqtrdi ⊢ ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) = { 𝑥 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ } )
329 316 148 317 328 syl3anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) = { 𝑥 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ } )
330 eqidd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
331 311 a1i ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V )
332 330 331 fvmpt2d ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) = if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
333 332 neeq1d ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ ↔ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ ) )
334 331 biantrurd ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ ↔ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V ∧ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ ) ) )
335 dif1o ⊢ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) ↔ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ V ∧ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ ) )
336 334 335 bitr4di ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ ↔ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) ) )
337 333 336 bitrd ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ ↔ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) ) )
338 337 rabbidva ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → { 𝑥 ∈ 𝐵 ∣ ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝐵 ∣ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) } )
339 329 338 eqtrd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) = { 𝑥 ∈ 𝐵 ∣ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) } )
340 311 335 mpbiran ⊢ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) ↔ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ )
341 ifeq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ∅ , ∅ ) )
342 341 179 eqtrdi ⊢ ( ( 𝐹 ‘ 𝑥 ) = ∅ → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = ∅ )
343 342 necon3i ⊢ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ → ( 𝐹 ‘ 𝑥 ) ≠ ∅ )
344 iffalse ⊢ ( ¬ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = ∅ )
345 344 necon1ai ⊢ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ → 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) )
346 343 345 jca ⊢ ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ → ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) )
347 256 expimpd ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝑥 ) ≠ ∅ ∧ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
348 346 347 syl5 ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ≠ ∅ → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
349 340 348 biimtrid ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
350 349 3impia ⊢ ( ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) ∧ 𝑥 ∈ 𝐵 ∧ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) ) → 𝑥 ∈ ( 𝑂 ‘ suc 𝑢 ) )
351 350 rabssdv ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → { 𝑥 ∈ 𝐵 ∣ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ∈ ( V ∖ 1o ) } ⊆ ( 𝑂 ‘ suc 𝑢 ) )
352 339 351 eqsstrd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) supp ∅ ) ⊆ ( 𝑂 ‘ suc 𝑢 ) )
353 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ↔ 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ) )
354 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ↔ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) )
355 353 354 orbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) ↔ ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) ) )
356 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
357 355 356 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
358 357 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
359 fveq2 ⊢ ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) )
360 359 adantl ⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) )
361 360 ifeq1da ⊢ ( 𝑦 ∈ 𝐵 → if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) = if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) )
362 354 356 ifbieq1d ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
363 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
364 363 175 ifex ⊢ if ( 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) ∈ V
365 362 314 364 fvmpt ⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) = if ( 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
366 365 ifeq2d ⊢ ( 𝑦 ∈ 𝐵 → if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) = if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , if ( 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) ) )
367 ifor ⊢ if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) = if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , if ( 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
368 366 367 eqtr4di ⊢ ( 𝑦 ∈ 𝐵 → if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑦 ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) = if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
369 361 368 eqtr3d ⊢ ( 𝑦 ∈ 𝐵 → if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) = if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
370 369 mpteq2ia ⊢ ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑦 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑦 ) , ∅ ) )
371 358 370 eqtr4i ⊢ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑦 ∈ 𝐵 ↦ if ( 𝑦 = ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) , ( ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ‘ 𝑦 ) ) )
372 1 151 148 186 202 208 352 371 cantnfp1 ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ∈ 𝑆 ∧ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) ) )
373 372 simprd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑥 = ( 𝑂 ‘ suc 𝑢 ) ∨ 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) )
374 309 373 eqtrd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) )
375 1 2 3 9 6 10 cantnfsuc ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ ω ) → ( 𝐻 ‘ suc suc 𝑢 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) )
376 192 375 syldan ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐻 ‘ suc suc 𝑢 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) )
377 160 simp3d ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
378 377 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
379 109 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = 𝑋 )
380 136 adantrr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑢 ∈ On )
381 onsssuc ⊢ ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On ∧ 𝑢 ∈ On ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ) )
382 129 380 381 syl2an2r ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ) )
383 146 382 mpbid ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 )
384 53 adantr ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 )
385 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂 ) ) → ( ( ◡ 𝑂 ‘ 𝑋 ) E suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) E ( 𝑂 ‘ suc 𝑢 ) ) )
386 240 384 143 385 syl12anc ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ◡ 𝑂 ‘ 𝑋 ) E suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) E ( 𝑂 ‘ suc 𝑢 ) ) )
387 243 epeli ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) E suc 𝑢 ↔ ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 )
388 245 epeli ⊢ ( ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) E ( 𝑂 ‘ suc 𝑢 ) ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) )
389 386 387 388 3bitr3g ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ↔ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
390 383 389 mpbid ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ ( 𝑂 ‘ suc 𝑢 ) )
391 379 390 eqeltrrd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → 𝑋 ∈ ( 𝑂 ‘ suc 𝑢 ) )
392 eleq2 ⊢ ( 𝑤 = ( 𝑂 ‘ suc 𝑢 ) → ( 𝑋 ∈ 𝑤 ↔ 𝑋 ∈ ( 𝑂 ‘ suc 𝑢 ) ) )
393 fveq2 ⊢ ( 𝑤 = ( 𝑂 ‘ suc 𝑢 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) )
394 fveq2 ⊢ ( 𝑤 = ( 𝑂 ‘ suc 𝑢 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) )
395 393 394 eqeq12d ⊢ ( 𝑤 = ( 𝑂 ‘ suc 𝑢 ) → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) = ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) )
396 392 395 imbi12d ⊢ ( 𝑤 = ( 𝑂 ‘ suc 𝑢 ) → ( ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑋 ∈ ( 𝑂 ‘ suc 𝑢 ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) = ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) ) )
397 396 rspcv ⊢ ( ( 𝑂 ‘ suc 𝑢 ) ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝑋 ∈ ( 𝑂 ‘ suc 𝑢 ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) = ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) ) )
398 202 378 391 397 syl3c ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) = ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) )
399 398 oveq2d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) = ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) )
400 399 oveq1d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐺 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) )
401 376 400 eqtr4d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( 𝐻 ‘ suc suc 𝑢 ) = ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) )
402 374 401 eleq12d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ↔ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ) ∈ ( ( ( 𝐴 ↑o ( 𝑂 ‘ suc 𝑢 ) ) ·o ( 𝐹 ‘ ( 𝑂 ‘ suc 𝑢 ) ) ) +o ( 𝐻 ‘ suc 𝑢 ) ) ) )
403 214 402 bitr4d ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
404 403 biimpd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
405 147 404 embantd ⊢ ( ( 𝜑 ∧ ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) ) → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
406 405 expr ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
407 140 406 sylbird ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
408 fveq2 ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) = ( 𝑂 ‘ suc 𝑢 ) )
409 408 sseq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) ) )
410 409 ifbid ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) = if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
411 410 mpteq2dv ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
412 411 fveq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
413 suceq ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → suc ( ◡ 𝑂 ‘ 𝑋 ) = suc suc 𝑢 )
414 413 fveq2d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) = ( 𝐻 ‘ suc suc 𝑢 ) )
415 412 414 eleq12d ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
416 115 415 syl5ibcom ⊢ ( 𝜑 → ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
417 416 adantr ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) )
418 417 a1dd ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
419 407 418 jaod ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ suc 𝑢 ∨ ( ◡ 𝑂 ‘ 𝑋 ) = suc 𝑢 ) → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
420 134 419 sylbid ⊢ ( ( 𝜑 ∧ suc 𝑢 ∈ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
421 420 expimpd ⊢ ( 𝜑 → ( ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
422 421 com23 ⊢ ( 𝜑 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) )
423 422 a1i ⊢ ( 𝑢 ∈ ω → ( 𝜑 → ( ( ( 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑢 ) ) → ( ( suc 𝑢 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ suc 𝑢 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ suc 𝑢 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc suc 𝑢 ) ) ) ) )
424 83 95 107 127 423 finds2 ⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( ( 𝑦 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ 𝑦 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc 𝑦 ) ) ) )
425 71 424 vtoclga ⊢ ( ∪ dom 𝑂 ∈ ω → ( 𝜑 → ( ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) ) ) )
426 58 425 mpcom ⊢ ( 𝜑 → ( ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ) → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) ) )
427 45 55 426 mp2and ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) ∈ ( 𝐻 ‘ suc ∪ dom 𝑂 ) )
428 155 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑥 ) ) )
429 eqeq2 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
430 eqeq2 ⊢ ( ∅ = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) → ( ( 𝐹 ‘ 𝑥 ) = ∅ ↔ ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
431 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
432 199 ffvelcdmi ⊢ ( ∪ dom 𝑂 ∈ dom 𝑂 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) )
433 45 432 syl ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝐺 supp ∅ ) )
434 197 433 sseldd ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝐵 )
435 onelon ⊢ ( ( 𝐵 ∈ On ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝐵 ) → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On )
436 3 434 435 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On )
437 436 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On )
438 ontri1 ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On ) → ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) )
439 224 437 438 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) )
440 439 con2bid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ) )
441 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → 𝑥 ∈ 𝐵 )
442 377 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) )
443 eloni ⊢ ( ( ◡ 𝑂 ‘ 𝑋 ) ∈ On → Ord ( ◡ 𝑂 ‘ 𝑋 ) )
444 129 443 syl ⊢ ( 𝜑 → Ord ( ◡ 𝑂 ‘ 𝑋 ) )
445 orduni ⊢ ( Ord dom 𝑂 → Ord ∪ dom 𝑂 )
446 37 445 ax-mp ⊢ Ord ∪ dom 𝑂
447 ordtri1 ⊢ ( ( Ord ( ◡ 𝑂 ‘ 𝑋 ) ∧ Ord ∪ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
448 444 446 447 sylancl ⊢ ( 𝜑 → ( ( ◡ 𝑂 ‘ 𝑋 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ) )
449 55 448 mpbid ⊢ ( 𝜑 → ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
450 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑋 ) ∈ dom 𝑂 ) ) → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
451 47 45 53 450 syl12anc ⊢ ( 𝜑 → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
452 fvex ⊢ ( ◡ 𝑂 ‘ 𝑋 ) ∈ V
453 452 epeli ⊢ ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑋 ) ↔ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) )
454 fvex ⊢ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ∈ V
455 454 epeli ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) )
456 451 453 455 3bitr3g ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ) )
457 109 eleq2d ⊢ ( 𝜑 → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑋 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
458 456 457 bitrd ⊢ ( 𝜑 → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑋 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
459 449 458 mtbid ⊢ ( 𝜑 → ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 )
460 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ On )
461 3 161 460 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ On )
462 ontri1 ⊢ ( ( 𝑋 ∈ On ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ On ) → ( 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
463 461 436 462 syl2anc ⊢ ( 𝜑 → ( 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ↔ ¬ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑋 ) )
464 459 463 mpbird ⊢ ( 𝜑 → 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) )
465 464 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) )
466 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 )
467 224 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → 𝑥 ∈ On )
468 ontr2 ⊢ ( ( 𝑋 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) → 𝑋 ∈ 𝑥 ) )
469 461 467 468 syl2an2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ( ( 𝑋 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) → 𝑋 ∈ 𝑥 ) )
470 465 466 469 mp2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → 𝑋 ∈ 𝑥 )
471 eleq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥 ) )
472 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
473 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑥 ) )
474 472 473 eqeq12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
475 471 474 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) ↔ ( 𝑋 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
476 475 rspcv ⊢ ( 𝑥 ∈ 𝐵 → ( ∀ 𝑤 ∈ 𝐵 ( 𝑋 ∈ 𝑤 → ( 𝐹 ‘ 𝑤 ) = ( 𝐺 ‘ 𝑤 ) ) → ( 𝑋 ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) )
477 441 442 470 476 syl3c ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
478 466 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 )
479 47 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) )
480 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ∪ dom 𝑂 ∈ dom 𝑂 )
481 52 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 )
482 ffvelcdm ⊢ ( ( ◡ 𝑂 : ( 𝐺 supp ∅ ) ⟶ dom 𝑂 ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 )
483 481 482 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 )
484 isorel ⊢ ( ( 𝑂 Isom E , E ( dom 𝑂 , ( 𝐺 supp ∅ ) ) ∧ ( ∪ dom 𝑂 ∈ dom 𝑂 ∧ ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 ) ) → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
485 479 480 483 484 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
486 269 epeli ⊢ ( ∪ dom 𝑂 E ( ◡ 𝑂 ‘ 𝑥 ) ↔ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) )
487 271 epeli ⊢ ( ( 𝑂 ‘ ∪ dom 𝑂 ) E ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) )
488 485 486 487 3bitr3g ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ) )
489 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → 𝑂 : dom 𝑂 –1-1-onto→ ( 𝐺 supp ∅ ) )
490 489 261 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) = 𝑥 )
491 490 eleq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ ( 𝑂 ‘ ( ◡ 𝑂 ‘ 𝑥 ) ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) )
492 488 491 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ↔ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) )
493 478 492 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) )
494 elssuni ⊢ ( ( ◡ 𝑂 ‘ 𝑥 ) ∈ dom 𝑂 → ( ◡ 𝑂 ‘ 𝑥 ) ⊆ ∪ dom 𝑂 )
495 483 494 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ⊆ ∪ dom 𝑂 )
496 37 483 275 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ◡ 𝑂 ‘ 𝑥 ) ∈ On )
497 496 277 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → Ord ( ◡ 𝑂 ‘ 𝑥 ) )
498 ordtri1 ⊢ ( ( Ord ( ◡ 𝑂 ‘ 𝑥 ) ∧ Ord ∪ dom 𝑂 ) → ( ( ◡ 𝑂 ‘ 𝑥 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ) )
499 497 446 498 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ( ( ◡ 𝑂 ‘ 𝑥 ) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) ) )
500 495 499 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) ∧ 𝑥 ∈ ( 𝐺 supp ∅ ) ) → ¬ ∪ dom 𝑂 ∈ ( ◡ 𝑂 ‘ 𝑥 ) )
501 493 500 pm2.65da ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ¬ 𝑥 ∈ ( 𝐺 supp ∅ ) )
502 441 501 eldifd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → 𝑥 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) )
503 ssidd ⊢ ( 𝜑 → ( 𝐺 supp ∅ ) ⊆ ( 𝐺 supp ∅ ) )
504 159 503 3 176 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ ( 𝐺 supp ∅ ) ) ) → ( 𝐺 ‘ 𝑥 ) = ∅ )
505 502 504 syldan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) = ∅ )
506 477 505 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
507 506 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑂 ‘ ∪ dom 𝑂 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
508 440 507 sylbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) → ( 𝐹 ‘ 𝑥 ) = ∅ ) )
509 508 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ¬ 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) ) → ( 𝐹 ‘ 𝑥 ) = ∅ )
510 429 430 431 509 ifbothda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) )
511 510 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
512 428 511 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) )
513 512 fveq2d ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ⊆ ( 𝑂 ‘ ∪ dom 𝑂 ) , ( 𝐹 ‘ 𝑥 ) , ∅ ) ) ) )
514 1 2 3 9 6 10 cantnfval ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = ( 𝐻 ‘ dom 𝑂 ) )
515 44 fveq2d ⊢ ( 𝜑 → ( 𝐻 ‘ dom 𝑂 ) = ( 𝐻 ‘ suc ∪ dom 𝑂 ) )
516 514 515 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) = ( 𝐻 ‘ suc ∪ dom 𝑂 ) )
517 427 513 516 3eltr4d ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( ( 𝐴 CNF 𝐵 ) ‘ 𝐺 ) )