MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cantnflem1 Structured version   Visualization version   GIF version

Theorem cantnflem1 8831
Description: Lemma for cantnf 8835. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation 𝑇 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 𝐹, 𝐺 are 𝑇 -related as 𝐹 < 𝐺 or 𝐺 < 𝐹, and WLOG assuming that 𝐹 < 𝐺, 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.)
Hypotheses
Ref Expression
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 ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐺‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
Assertion
Ref Expression
cantnflem1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Distinct variable groups:   𝑘,𝑐,𝑤,𝑥,𝑦,𝑧,𝐵   𝐴,𝑐,𝑘,𝑤,𝑥,𝑦,𝑧   𝑇,𝑐,𝑘   𝑘,𝐹,𝑤,𝑥,𝑦,𝑧   𝑆,𝑐,𝑘,𝑥,𝑦,𝑧   𝐺,𝑐,𝑘,𝑤,𝑥,𝑦,𝑧   𝑥,𝐻,𝑦   𝑘,𝑂,𝑤,𝑥,𝑦,𝑧   𝜑,𝑘,𝑥,𝑦,𝑧   𝑘,𝑋,𝑤,𝑥,𝑦,𝑧   𝐹,𝑐   𝜑,𝑐
Allowed substitution hints:   𝜑(𝑤)   𝑆(𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)   𝐻(𝑧,𝑤,𝑘,𝑐)   𝑂(𝑐)   𝑋(𝑐)

Proof of Theorem cantnflem1
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 ovex 6904 . . . . . 6 (𝐺 supp ∅) ∈ V
2 cantnflem1.o . . . . . . 7 𝑂 = OrdIso( E , (𝐺 supp ∅))
32oion 8678 . . . . . 6 ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
41, 3mp1i 13 . . . . 5 (𝜑 → dom 𝑂 ∈ On)
5 uniexg 7183 . . . . 5 (dom 𝑂 ∈ On → dom 𝑂 ∈ V)
6 sucidg 6014 . . . . 5 ( dom 𝑂 ∈ V → dom 𝑂 ∈ suc dom 𝑂)
74, 5, 63syl 18 . . . 4 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
8 cantnfs.s . . . . . . . . . 10 𝑆 = dom (𝐴 CNF 𝐵)
9 cantnfs.a . . . . . . . . . 10 (𝜑𝐴 ∈ On)
10 cantnfs.b . . . . . . . . . 10 (𝜑𝐵 ∈ On)
11 oemapval.t . . . . . . . . . 10 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐵 ((𝑥𝑧) ∈ (𝑦𝑧) ∧ ∀𝑤𝐵 (𝑧𝑤 → (𝑥𝑤) = (𝑦𝑤)))}
12 oemapval.f . . . . . . . . . 10 (𝜑𝐹𝑆)
13 oemapval.g . . . . . . . . . 10 (𝜑𝐺𝑆)
14 oemapvali.r . . . . . . . . . 10 (𝜑𝐹𝑇𝐺)
15 oemapvali.x . . . . . . . . . 10 𝑋 = {𝑐𝐵 ∣ (𝐹𝑐) ∈ (𝐺𝑐)}
168, 9, 10, 11, 12, 13, 14, 15cantnflem1a 8827 . . . . . . . . 9 (𝜑𝑋 ∈ (𝐺 supp ∅))
17 n0i 4119 . . . . . . . . 9 (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19 ovexd 6906 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) ∈ V)
208, 9, 10, 2, 13cantnfcl 8809 . . . . . . . . . . 11 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
2120simpld 484 . . . . . . . . . 10 (𝜑 → E We (𝐺 supp ∅))
222oien 8680 . . . . . . . . . 10 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
2319, 21, 22syl2anc 575 . . . . . . . . 9 (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24 breq1 4845 . . . . . . . . . 10 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25 ensymb 8238 . . . . . . . . . . 11 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26 en0 8253 . . . . . . . . . . 11 ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
2725, 26bitri 266 . . . . . . . . . 10 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
2824, 27syl6bb 278 . . . . . . . . 9 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
2923, 28syl5ibcom 236 . . . . . . . 8 (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
3018, 29mtod 189 . . . . . . 7 (𝜑 → ¬ dom 𝑂 = ∅)
3120simprd 485 . . . . . . . 8 (𝜑 → dom 𝑂 ∈ ω)
32 nnlim 7306 . . . . . . . 8 (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
3331, 32syl 17 . . . . . . 7 (𝜑 → ¬ Lim dom 𝑂)
34 ioran 997 . . . . . . 7 (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
3530, 33, 34sylanbrc 574 . . . . . 6 (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
362oicl 8671 . . . . . . 7 Ord dom 𝑂
37 unizlim 6055 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3836, 37mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3935, 38mtbird 316 . . . . 5 (𝜑 → ¬ dom 𝑂 = dom 𝑂)
40 orduniorsuc 7258 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4136, 40mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4241ord 882 . . . . 5 (𝜑 → (¬ dom 𝑂 = dom 𝑂 → dom 𝑂 = suc dom 𝑂))
4339, 42mpd 15 . . . 4 (𝜑 → dom 𝑂 = suc dom 𝑂)
447, 43eleqtrrd 2886 . . 3 (𝜑 dom 𝑂 ∈ dom 𝑂)
452oiiso 8679 . . . . . . . 8 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
4619, 21, 45syl2anc 575 . . . . . . 7 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47 isof1o 6795 . . . . . . 7 (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
4846, 47syl 17 . . . . . 6 (𝜑𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
49 f1ocnv 6363 . . . . . 6 (𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) → 𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50 f1of 6351 . . . . . 6 (𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5148, 49, 503syl 18 . . . . 5 (𝜑𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5251, 16ffvelrnd 6580 . . . 4 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
53 elssuni 4659 . . . 4 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5452, 53syl 17 . . 3 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
5543, 31eqeltrrd 2884 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
56 peano2b 7309 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
5755, 56sylibr 225 . . . 4 (𝜑 dom 𝑂 ∈ ω)
58 eleq1 2871 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝑦 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
59 sseq2 3822 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ dom 𝑂))
6058, 59anbi12d 618 . . . . . . 7 (𝑦 = dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂)))
61 fveq2 6406 . . . . . . . . . . . 12 (𝑦 = dom 𝑂 → (𝑂𝑦) = (𝑂 dom 𝑂))
6261sseq2d 3828 . . . . . . . . . . 11 (𝑦 = dom 𝑂 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂 dom 𝑂)))
6362ifbid 4299 . . . . . . . . . 10 (𝑦 = dom 𝑂 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
6463mpteq2dv 4937 . . . . . . . . 9 (𝑦 = dom 𝑂 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
6564fveq2d 6410 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
66 suceq 6001 . . . . . . . . 9 (𝑦 = dom 𝑂 → suc 𝑦 = suc dom 𝑂)
6766fveq2d 6410 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc dom 𝑂))
6865, 67eleq12d 2877 . . . . . . 7 (𝑦 = dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
6960, 68imbi12d 335 . . . . . 6 (𝑦 = dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
7069imbi2d 331 . . . . 5 (𝑦 = dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))))
71 eleq1 2871 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72 sseq2 3822 . . . . . . . 8 (𝑦 = ∅ → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ ∅))
7371, 72anbi12d 618 . . . . . . 7 (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅)))
74 fveq2 6406 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑂𝑦) = (𝑂‘∅))
7574sseq2d 3828 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
7675ifbid 4299 . . . . . . . . . 10 (𝑦 = ∅ → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
7776mpteq2dv 4937 . . . . . . . . 9 (𝑦 = ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
7877fveq2d 6410 . . . . . . . 8 (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
79 suceq 6001 . . . . . . . . 9 (𝑦 = ∅ → suc 𝑦 = suc ∅)
8079fveq2d 6410 . . . . . . . 8 (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
8178, 80eleq12d 2877 . . . . . . 7 (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
8273, 81imbi12d 335 . . . . . 6 (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83 eleq1 2871 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂𝑢 ∈ dom 𝑂))
84 sseq2 3822 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ 𝑢))
8583, 84anbi12d 618 . . . . . . 7 (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)))
86 fveq2 6406 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑂𝑦) = (𝑂𝑢))
8786sseq2d 3828 . . . . . . . . . . 11 (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂𝑢)))
8887ifbid 4299 . . . . . . . . . 10 (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
8988mpteq2dv 4937 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
9089fveq2d 6410 . . . . . . . 8 (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))
91 suceq 6001 . . . . . . . . 9 (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
9291fveq2d 6410 . . . . . . . 8 (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
9390, 92eleq12d 2877 . . . . . . 7 (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
9485, 93imbi12d 335 . . . . . 6 (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95 eleq1 2871 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96 sseq2 3822 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ suc 𝑢))
9795, 96anbi12d 618 . . . . . . 7 (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢)))
98 fveq2 6406 . . . . . . . . . . . 12 (𝑦 = suc 𝑢 → (𝑂𝑦) = (𝑂‘suc 𝑢))
9998sseq2d 3828 . . . . . . . . . . 11 (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
10099ifbid 4299 . . . . . . . . . 10 (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
101100mpteq2dv 4937 . . . . . . . . 9 (𝑦 = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
102101fveq2d 6410 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
103 suceq 6001 . . . . . . . . 9 (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104103fveq2d 6410 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105102, 104eleq12d 2877 . . . . . . 7 (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
10697, 105imbi12d 335 . . . . . 6 (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107 f1ocnvfv2 6755 . . . . . . . . . . . . 13 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
10848, 16, 107syl2anc 575 . . . . . . . . . . . 12 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
109108sseq2d 3828 . . . . . . . . . . 11 (𝜑 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥𝑋))
110109ifbid 4299 . . . . . . . . . 10 (𝜑 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥𝑋, (𝐹𝑥), ∅))
111110mpteq2dv 4937 . . . . . . . . 9 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅)))
112111fveq2d 6410 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))))
113 cantnflem1.h . . . . . . . . 9 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐺‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 8830 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
115112, 114eqeltrd 2883 . . . . . . 7 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
116 ss0 4170 . . . . . . . . . . . . . 14 ((𝑂𝑋) ⊆ ∅ → (𝑂𝑋) = ∅)
117116fveq2d 6410 . . . . . . . . . . . . 13 ((𝑂𝑋) ⊆ ∅ → (𝑂‘(𝑂𝑋)) = (𝑂‘∅))
118117sseq2d 3828 . . . . . . . . . . . 12 ((𝑂𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119118ifbid 4299 . . . . . . . . . . 11 ((𝑂𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
120119mpteq2dv 4937 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
121120fveq2d 6410 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
122 suceq 6001 . . . . . . . . . . 11 ((𝑂𝑋) = ∅ → suc (𝑂𝑋) = suc ∅)
123116, 122syl 17 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → suc (𝑂𝑋) = suc ∅)
124123fveq2d 6410 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc ∅))
125121, 124eleq12d 2877 . . . . . . . 8 ((𝑂𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126125adantl 469 . . . . . . 7 ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127115, 126syl5ibcom 236 . . . . . 6 (𝜑 → ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128 ordelon 5958 . . . . . . . . . . . . 13 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
12936, 52, 128sylancr 577 . . . . . . . . . . . 12 (𝜑 → (𝑂𝑋) ∈ On)
130129adantr 468 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
13136a1i 11 . . . . . . . . . . . 12 (𝜑 → Ord dom 𝑂)
132 ordelon 5958 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133131, 132sylan 571 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
134 onsseleq 5976 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
135130, 133, 134syl2anc 575 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
136 sucelon 7245 . . . . . . . . . . . . . . 15 (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
137133, 136sylibr 225 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
138 eloni 5944 . . . . . . . . . . . . . 14 (𝑢 ∈ On → Ord 𝑢)
139137, 138syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
140 ordsssuc 6023 . . . . . . . . . . . . 13 (((𝑂𝑋) ∈ On ∧ Ord 𝑢) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
141130, 139, 140syl2anc 575 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
142 ordtr 5948 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → Tr dom 𝑂)
14336, 142mp1i 13 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
144 simprl 778 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
145 trsuc 6021 . . . . . . . . . . . . . . . 16 ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
146143, 144, 145syl2anc 575 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
147 simprr 780 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ⊆ 𝑢)
148146, 147jca 503 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢))
1499adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
15010adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
151 oecl 7852 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
152149, 150, 151syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 𝐵) ∈ On)
1538, 149, 150cantnff 8816 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
1548, 9, 10cantnfs 8808 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
15512, 154mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
156155simpld 484 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝐵𝐴)
157156ffvelrnda 6579 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → (𝐹𝑥) ∈ 𝐴)
1588, 9, 10cantnfs 8808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
15913, 158mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
160159simpld 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺:𝐵𝐴)
1618, 9, 10, 11, 12, 13, 14, 15oemapvali 8826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑋𝐵 ∧ (𝐹𝑋) ∈ (𝐺𝑋) ∧ ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤))))
162161simp1d 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
163160, 162ffvelrnd 6580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐺𝑋) ∈ 𝐴)
164163ne0d 4121 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ≠ ∅)
165 on0eln0 5991 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
1669, 165syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∅ ∈ 𝐴𝐴 ≠ ∅))
167164, 166mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∅ ∈ 𝐴)
168167adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → ∅ ∈ 𝐴)
169157, 168ifcld 4322 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ 𝐴)
170169fmpttd 6605 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴)
171 mptexg 6707 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ On → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
17210, 171syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
173 funmpt 6137 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
174173a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
175155simprd 485 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 finSupp ∅)
176 ssidd 3819 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
177 0ex 4982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ V
178177a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∅ ∈ V)
179156, 176, 10, 178suppssr 7559 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑥) = ∅)
180179ifeq1d 4295 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
181 ifid 4316 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑥 ⊆ (𝑂𝑢), ∅, ∅) = ∅
182180, 181syl6eq 2854 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
183182, 10suppss2 7562 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
184 fsuppsssupp 8528 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V ∧ Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
185172, 174, 175, 183, 184syl22anc 858 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
1868, 9, 10cantnfs 8808 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴 ∧ (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)))
187170, 185, 186mpbir2and 695 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
188187adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
189153, 188ffvelrnd 6580 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵))
190 onelon 5959 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
191152, 189, 190syl2anc 575 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
19231adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
193 elnn 7303 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
194144, 192, 193syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
195113cantnfvalf 8807 . . . . . . . . . . . . . . . . . . 19 𝐻:ω⟶On
196195ffvelrni 6578 . . . . . . . . . . . . . . . . . 18 (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
197194, 196syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
198 suppssdm 7540 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
199198, 160fssdm 6270 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
200199adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
2012oif 8672 . . . . . . . . . . . . . . . . . . . . . . 23 𝑂:dom 𝑂⟶(𝐺 supp ∅)
202201ffvelrni 6578 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
203144, 202syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
204200, 203sseldd 3797 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
205 onelon 5959 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
206150, 204, 205syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
207 oecl 7852 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
208149, 206, 207syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
209156adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐹:𝐵𝐴)
210209, 204ffvelrnd 6580 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
211 onelon 5959 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
212149, 210, 211syl2anc 575 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
213 omcl 7851 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
214208, 212, 213syl2anc 575 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
215 oaord 7862 . . . . . . . . . . . . . . . . 17 ((((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
216191, 197, 214, 215syl3anc 1483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
217 ifeq1 4281 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
218 ifid 4316 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
219217, 218syl6eq 2854 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = ∅)
220 ifeq1 4281 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅))
221 ifid 4316 . . . . . . . . . . . . . . . . . . . . . . 23 if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅) = ∅
222220, 221syl6eq 2854 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = ∅)
223219, 222eqeq12d 2819 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) ↔ ∅ = ∅))
224 onss 7218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → 𝐵 ⊆ On)
22510, 224syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ⊆ On)
226225sselda 3796 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐵) → 𝑥 ∈ On)
227226adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → 𝑥 ∈ On)
228206adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑂‘suc 𝑢) ∈ On)
229 onsseleq 5976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
230227, 228, 229syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
231230adantr 468 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
232227adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → 𝑥 ∈ On)
233201ffvelrni 6578 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ dom 𝑂 → (𝑂𝑢) ∈ (𝐺 supp ∅))
234146, 233syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝐺 supp ∅))
235200, 234sseldd 3797 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ 𝐵)
236 onelon 5959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ (𝑂𝑢) ∈ 𝐵) → (𝑂𝑢) ∈ On)
237150, 235, 236syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ On)
238237ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑂𝑢) ∈ On)
239 onsssuc 6024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
240232, 238, 239syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
241 vex 3392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑢 ∈ V
242241sucid 6015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ suc 𝑢
24346adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
244 isorel 6798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
245243, 146, 144, 244syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
246241sucex 7239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc 𝑢 ∈ V
247246epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 E suc 𝑢𝑢 ∈ suc 𝑢)
248 fvex 6419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑂‘suc 𝑢) ∈ V
249248epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
250245, 247, 2493bitr3g 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢)))
251242, 250mpbii 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
252 eloni 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
253206, 252syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
254 ordelsuc 7248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑂𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
255237, 253, 254syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
256251, 255mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
257256ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
258257sseld 3795 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
259240, 258sylbid 231 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
260 simprr 780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ 𝑥)
261243ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
262261, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
2638, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 8829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
264 f1ocnvfv2 6755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
265262, 263, 264syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂‘(𝑂𝑥)) = 𝑥)
266260, 265eleqtrrd 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
267146ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
268262, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
269268, 263ffvelrnd 6580 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ dom 𝑂)
270 isorel 6798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
271261, 267, 269, 270syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
272 fvex 6419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂𝑥) ∈ V
273272epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 E (𝑂𝑥) ↔ 𝑢 ∈ (𝑂𝑥))
274 fvex 6419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂‘(𝑂𝑥)) ∈ V
275274epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑢) E (𝑂‘(𝑂𝑥)) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
276271, 273, 2753bitr3g 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥))))
277266, 276mpbird 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ (𝑂𝑥))
278 ordelon 5958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂) → (𝑂𝑥) ∈ On)
27936, 269, 278sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ On)
280 eloni 5944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑥) ∈ On → Ord (𝑂𝑥))
281279, 280syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → Ord (𝑂𝑥))
282 ordelsuc 7248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢 ∈ (𝑂𝑥) ∧ Ord (𝑂𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
283277, 281, 282syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
284277, 283mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (𝑂𝑥))
285144ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
28636, 285, 132sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
287 ontri1 5968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc 𝑢 ∈ On ∧ (𝑂𝑥) ∈ On) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
288286, 279, 287syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
289284, 288mpbid 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ (𝑂𝑥) ∈ suc 𝑢)
290 isorel 6798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
291261, 269, 285, 290syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
292246epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑥) E suc 𝑢 ↔ (𝑂𝑥) ∈ suc 𝑢)
293248epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢))
294291, 292, 2933bitr3g 304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢)))
295265eleq1d 2868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
296294, 295bitrd 270 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢𝑥 ∈ (𝑂‘suc 𝑢)))
297289, 296mtbid 315 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
298297expr 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑂𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
299298con2d 131 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂𝑢) ∈ 𝑥))
300 ontri1 5968 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
301232, 238, 300syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
302299, 301sylibrd 250 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂𝑢)))
303259, 302impbid 203 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
304303orbi1d 931 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
305231, 304bitr4d 273 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
306 orcom 888 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)))
307305, 306syl6bb 278 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢))))
308307ifbid 4299 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
309 eqidd 2805 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ∅ = ∅)
310223, 308, 309pm2.61ne 3061 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
311310mpteq2dva 4936 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)))
312311fveq2d 6410 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))))
313 fvex 6419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑥) ∈ V
314313, 177ifex 4325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V
315314a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
316315ralrimivw 3153 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
317 eqid 2804 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
318317fnmpt 6229 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
319316, 318syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
320177a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∅ ∈ V)
321 suppvalfn 7534 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅})
322 nfcv 2946 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝐵
323 nfcv 2946 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐵
324 nffvmpt1 6417 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)
325 nfcv 2946 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥
326324, 325nfne 3076 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅
327 nfv 2005 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅
328 fveq2 6406 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥))
329328neeq1d 3035 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅))
330322, 323, 326, 327, 329cbvrab 3386 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅}
331321, 330syl6eq 2854 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
332319, 150, 320, 331syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
333 eqidd 2805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
334314a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
335333, 334fvmpt2d 6512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
336335neeq1d 3035 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
337334biantrurd 524 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)))
338 dif1o 7815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
339337, 338syl6bbr 280 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)))
340336, 339bitrd 270 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)))
341340rabbidva 3376 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
342332, 341eqtrd 2838 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
343314, 338mpbiran 691 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)
344 ifeq1 4281 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
345344, 181syl6eq 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
346345necon3i 3008 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → (𝐹𝑥) ≠ ∅)
347 iffalse 4286 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ⊆ (𝑂𝑢) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
348347necon1ai 3003 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂𝑢))
349346, 348jca 503 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → ((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)))
350259expimpd 443 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
351349, 350syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
352343, 351syl5bi 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) → 𝑥 ∈ (𝑂‘suc 𝑢)))
3533523impia 1138 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵 ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
354353rabssdv 3877 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
355342, 354eqsstrd 3834 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
356 eqeq1 2808 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
357 sseq1 3821 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑦 ⊆ (𝑂𝑢)))
358356, 357orbi12d 933 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢))))
359 fveq2 6406 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
360358, 359ifbieq1d 4300 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
361360cbvmptv 4942 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
362 fveq2 6406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑂‘suc 𝑢) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
363362adantl 469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐵𝑦 = (𝑂‘suc 𝑢)) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
364363ifeq1da 4307 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
365357, 359ifbieq1d 4300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
366 fvex 6419 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑦) ∈ V
367366, 177ifex 4325 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅) ∈ V
368365, 317, 367fvmpt 6501 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
369368ifeq2d 4296 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅)))
370 ifor 4329 . . . . . . . . . . . . . . . . . . . . . . . 24 if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
371369, 370syl6eqr 2856 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
372364, 371eqtr3d 2840 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
373372mpteq2ia 4932 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦))) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
374361, 373eqtr4i 2829 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
3758, 149, 150, 188, 204, 210, 355, 374cantnfp1 8823 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))))
376375simprd 485 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
377312, 376eqtrd 2838 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
3788, 9, 10, 2, 13, 113cantnfsuc 8812 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
379194, 378syldan 581 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
380161simp3d 1167 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
381380adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
382108adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) = 𝑋)
383129adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ On)
384137adantrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
385 onsssuc 6024 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑂𝑋) ∈ On ∧ 𝑢 ∈ On) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
386383, 384, 385syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
387147, 386mpbid 223 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ suc 𝑢)
38852adantr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ dom 𝑂)
389 isorel 6798 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
390243, 388, 144, 389syl12anc 856 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
391246epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂𝑋) E suc 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢)
392248epeli 5224 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
393390, 391, 3923bitr3g 304 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢)))
394387, 393mpbid 223 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
395382, 394eqeltrrd 2884 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
396 eleq2 2872 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → (𝑋𝑤𝑋 ∈ (𝑂‘suc 𝑢)))
397 fveq2 6406 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐹𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
398 fveq2 6406 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐺𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
399397, 398eqeq12d 2819 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
400396, 399imbi12d 335 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑂‘suc 𝑢) → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
401400rspcv 3496 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
402204, 381, 395, 401syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
403402oveq2d 6888 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
404403oveq1d 6887 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
405379, 404eqtr4d 2841 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
406377, 405eleq12d 2877 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
407216, 406bitr4d 273 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
408407biimpd 220 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
409148, 408embantd 59 . . . . . . . . . . . . 13 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
410409expr 446 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
411141, 410sylbird 251 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
412 fveq2 6406 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑋) = suc 𝑢 → (𝑂‘(𝑂𝑋)) = (𝑂‘suc 𝑢))
413412sseq2d 3828 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
414413ifbid 4299 . . . . . . . . . . . . . . . . 17 ((𝑂𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
415414mpteq2dv 4937 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
416415fveq2d 6410 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
417 suceq 6001 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → suc (𝑂𝑋) = suc suc 𝑢)
418417fveq2d 6410 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc suc 𝑢))
419416, 418eleq12d 2877 . . . . . . . . . . . . . 14 ((𝑂𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
420115, 419syl5ibcom 236 . . . . . . . . . . . . 13 (𝜑 → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
421420adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
422421a1dd 50 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
423411, 422jaod 877 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
424135, 423sylbid 231 . . . . . . . . 9 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
425424expimpd 443 . . . . . . . 8 (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
426425com23 86 . . . . . . 7 (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
427426a1i 11 . . . . . 6 (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
42882, 94, 106, 127, 427finds2 7322 . . . . 5 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
42970, 428vtoclga 3463 . . . 4 ( dom 𝑂 ∈ ω → (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
43057, 429mpcom 38 . . 3 (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
43144, 54, 430mp2and 682 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))
432156feqmptd 6468 . . . 4 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
433 eqeq2 2815 . . . . . 6 ((𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = (𝐹𝑥) ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
434 eqeq2 2815 . . . . . 6 (∅ = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = ∅ ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
435 eqidd 2805 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = (𝐹𝑥))
436201ffvelrni 6578 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
43744, 436syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
438199, 437sseldd 3797 . . . . . . . . . . . 12 (𝜑 → (𝑂 dom 𝑂) ∈ 𝐵)
439 onelon 5959 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑂 dom 𝑂) ∈ 𝐵) → (𝑂 dom 𝑂) ∈ On)
44010, 438, 439syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) ∈ On)
441440adantr 468 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑂 dom 𝑂) ∈ On)
442 ontri1 5968 . . . . . . . . . 10 ((𝑥 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
443226, 441, 442syl2anc 575 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
444443con2bid 345 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)))
445 simprl 778 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥𝐵)
446380adantr 468 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
447 eloni 5944 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) ∈ On → Ord (𝑂𝑋))
448129, 447syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord (𝑂𝑋))
449 orduni 7222 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑂 → Ord dom 𝑂)
45036, 449ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord dom 𝑂
451 ordtri1 5967 . . . . . . . . . . . . . . . . 17 ((Ord (𝑂𝑋) ∧ Ord dom 𝑂) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
452448, 450, 451sylancl 576 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
45354, 452mpbid 223 . . . . . . . . . . . . . . 15 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
454 isorel 6798 . . . . . . . . . . . . . . . . . 18 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
45546, 44, 52, 454syl12anc 856 . . . . . . . . . . . . . . . . 17 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
456 fvex 6419 . . . . . . . . . . . . . . . . . 18 (𝑂𝑋) ∈ V
457456epeli 5224 . . . . . . . . . . . . . . . . 17 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
458 fvex 6419 . . . . . . . . . . . . . . . . . 18 (𝑂‘(𝑂𝑋)) ∈ V
459458epeli 5224 . . . . . . . . . . . . . . . . 17 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
460455, 457, 4593bitr3g 304 . . . . . . . . . . . . . . . 16 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
461108eleq2d 2869 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
462460, 461bitrd 270 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
463453, 462mtbid 315 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
464 onelon 5959 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
46510, 162, 464syl2anc 575 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ On)
466 ontri1 5968 . . . . . . . . . . . . . . 15 ((𝑋 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
467465, 440, 466syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
468463, 467mpbird 248 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (𝑂 dom 𝑂))
469468adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂 dom 𝑂))
470 simprr 780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝑂 dom 𝑂) ∈ 𝑥)
471465adantr 468 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
472226adantrr 699 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
473 ontr2 5983 . . . . . . . . . . . . 13 ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
474471, 472, 473syl2anc 575 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
475469, 470, 474mp2and 682 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋𝑥)
476 eleq2 2872 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑋𝑤𝑋𝑥))
477 fveq2 6406 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
478 fveq2 6406 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐺𝑤) = (𝐺𝑥))
479477, 478eqeq12d 2819 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹𝑥) = (𝐺𝑥)))
480476, 479imbi12d 335 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
481480rspcv 3496 . . . . . . . . . . 11 (𝑥𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
482445, 446, 475, 481syl3c 66 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = (𝐺𝑥))
483470adantr 468 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂 dom 𝑂) ∈ 𝑥)
48446ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
48544ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ dom 𝑂)
48651ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
487 ffvelrn 6577 . . . . . . . . . . . . . . . . . 18 ((𝑂:(𝐺 supp ∅)⟶dom 𝑂𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
488486, 487sylancom 578 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
489 isorel 6798 . . . . . . . . . . . . . . . . 17 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
490484, 485, 488, 489syl12anc 856 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
491272epeli 5224 . . . . . . . . . . . . . . . 16 ( dom 𝑂 E (𝑂𝑥) ↔ dom 𝑂 ∈ (𝑂𝑥))
492274epeli 5224 . . . . . . . . . . . . . . . 16 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)))
493490, 491, 4923bitr3g 304 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥))))
49448ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
495494, 264sylancom 578 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
496495eleq2d 2869 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
497493, 496bitrd 270 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
498483, 497mpbird 248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ (𝑂𝑥))
499 elssuni 4659 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∈ dom 𝑂 → (𝑂𝑥) ⊆ dom 𝑂)
500488, 499syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ⊆ dom 𝑂)
50136, 488, 278sylancr 577 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ On)
502501, 280syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (𝑂𝑥))
503 ordtri1 5967 . . . . . . . . . . . . . . 15 ((Ord (𝑂𝑥) ∧ Ord dom 𝑂) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
504502, 450, 503sylancl 576 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
505500, 504mpbid 223 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ dom 𝑂 ∈ (𝑂𝑥))
506498, 505pm2.65da 842 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
507445, 506eldifd 3778 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
508 ssidd 3819 . . . . . . . . . . . 12 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
509160, 508, 10, 178suppssr 7559 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑥) = ∅)
510507, 509syldan 581 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐺𝑥) = ∅)
511482, 510eqtrd 2838 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = ∅)
512511expr 446 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 → (𝐹𝑥) = ∅))
513444, 512sylbird 251 . . . . . . 7 ((𝜑𝑥𝐵) → (¬ 𝑥 ⊆ (𝑂 dom 𝑂) → (𝐹𝑥) = ∅))
514513imp 395 . . . . . 6 (((𝜑𝑥𝐵) ∧ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = ∅)
515433, 434, 435, 514ifbothda 4314 . . . . 5 ((𝜑𝑥𝐵) → (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
516515mpteq2dva 4936 . . . 4 (𝜑 → (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
517432, 516eqtrd 2838 . . 3 (𝜑𝐹 = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
518517fveq2d 6410 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
5198, 9, 10, 2, 13, 113cantnfval 8810 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
52043fveq2d 6410 . . 3 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
521519, 520eqtrd 2838 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc dom 𝑂))
522431, 518, 5213eltr4d 2898 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wcel 2156  wne 2976  wral 3094  wrex 3095  {crab 3098  Vcvv 3389  cdif 3764  wss 3767  c0 4114  ifcif 4277   cuni 4628   class class class wbr 4842  {copab 4904  cmpt 4921  Tr wtr 4944   E cep 5221   We wwe 5267  ccnv 5308  dom cdm 5309  Ord word 5933  Oncon0 5934  Lim wlim 5935  suc csuc 5936  Fun wfun 6093   Fn wfn 6094  wf 6095  1-1-ontowf1o 6098  cfv 6099   Isom wiso 6100  (class class class)co 6872  cmpt2 6874  ωcom 7293   supp csupp 7527  seq𝜔cseqom 7776  1𝑜c1o 7787   +𝑜 coa 7791   ·𝑜 comu 7792  𝑜 coe 7793  cen 8187   finSupp cfsupp 8512  OrdIsocoi 8651   CNF ccnf 8803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-rep 4962  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5094  ax-un 7177
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-ne 2977  df-ral 3099  df-rex 3100  df-reu 3101  df-rmo 3102  df-rab 3103  df-v 3391  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4115  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-tp 4373  df-op 4375  df-uni 4629  df-int 4668  df-iun 4712  df-br 4843  df-opab 4905  df-mpt 4922  df-tr 4945  df-id 5217  df-eprel 5222  df-po 5230  df-so 5231  df-fr 5268  df-se 5269  df-we 5270  df-xp 5315  df-rel 5316  df-cnv 5317  df-co 5318  df-dm 5319  df-rn 5320  df-res 5321  df-ima 5322  df-pred 5891  df-ord 5937  df-on 5938  df-lim 5939  df-suc 5940  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-isom 6108  df-riota 6833  df-ov 6875  df-oprab 6876  df-mpt2 6877  df-om 7294  df-1st 7396  df-2nd 7397  df-supp 7528  df-wrecs 7640  df-recs 7702  df-rdg 7740  df-seqom 7777  df-1o 7794  df-2o 7795  df-oadd 7798  df-omul 7799  df-oexp 7800  df-er 7977  df-map 8092  df-en 8191  df-dom 8192  df-sdom 8193  df-fin 8194  df-fsupp 8513  df-oi 8652  df-cnf 8804
This theorem is referenced by:  cantnf  8835
  Copyright terms: Public domain W3C validator