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

Theorem cantnflem1 8759
Description: Lemma for cantnf 8763. 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 6841 . . . . . 6 (𝐺 supp ∅) ∈ V
2 cantnflem1.o . . . . . . 7 𝑂 = OrdIso( E , (𝐺 supp ∅))
32oion 8606 . . . . . 6 ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
41, 3mp1i 13 . . . . 5 (𝜑 → dom 𝑂 ∈ On)
5 uniexg 7120 . . . . 5 (dom 𝑂 ∈ On → dom 𝑂 ∈ V)
6 sucidg 5964 . . . . 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 8755 . . . . . . . . 9 (𝜑𝑋 ∈ (𝐺 supp ∅))
17 n0i 4063 . . . . . . . . 9 (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19 ovexd 6843 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) ∈ V)
208, 9, 10, 2, 13cantnfcl 8737 . . . . . . . . . . 11 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
2120simpld 477 . . . . . . . . . 10 (𝜑 → E We (𝐺 supp ∅))
222oien 8608 . . . . . . . . . 10 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
2319, 21, 22syl2anc 696 . . . . . . . . 9 (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24 breq1 4807 . . . . . . . . . 10 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25 ensymb 8169 . . . . . . . . . . 11 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26 en0 8184 . . . . . . . . . . 11 ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
2725, 26bitri 264 . . . . . . . . . 10 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
2824, 27syl6bb 276 . . . . . . . . 9 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
2923, 28syl5ibcom 235 . . . . . . . 8 (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
3018, 29mtod 189 . . . . . . 7 (𝜑 → ¬ dom 𝑂 = ∅)
3120simprd 482 . . . . . . . 8 (𝜑 → dom 𝑂 ∈ ω)
32 nnlim 7243 . . . . . . . 8 (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
3331, 32syl 17 . . . . . . 7 (𝜑 → ¬ Lim dom 𝑂)
34 ioran 512 . . . . . . 7 (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
3530, 33, 34sylanbrc 701 . . . . . 6 (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
362oicl 8599 . . . . . . 7 Ord dom 𝑂
37 unizlim 6005 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3836, 37mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3935, 38mtbird 314 . . . . 5 (𝜑 → ¬ dom 𝑂 = dom 𝑂)
40 orduniorsuc 7195 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4136, 40mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4241ord 391 . . . . 5 (𝜑 → (¬ dom 𝑂 = dom 𝑂 → dom 𝑂 = suc dom 𝑂))
4339, 42mpd 15 . . . 4 (𝜑 → dom 𝑂 = suc dom 𝑂)
447, 43eleqtrrd 2842 . . 3 (𝜑 dom 𝑂 ∈ dom 𝑂)
452oiiso 8607 . . . . . . . 8 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
4619, 21, 45syl2anc 696 . . . . . . 7 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47 isof1o 6736 . . . . . . 7 (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
4846, 47syl 17 . . . . . 6 (𝜑𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
49 f1ocnv 6310 . . . . . 6 (𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) → 𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50 f1of 6298 . . . . . 6 (𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5148, 49, 503syl 18 . . . . 5 (𝜑𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5251, 16ffvelrnd 6523 . . . 4 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
53 elssuni 4619 . . . 4 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5452, 53syl 17 . . 3 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
5543, 31eqeltrrd 2840 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
56 peano2b 7246 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
5755, 56sylibr 224 . . . 4 (𝜑 dom 𝑂 ∈ ω)
58 eleq1 2827 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝑦 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
59 sseq2 3768 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ dom 𝑂))
6058, 59anbi12d 749 . . . . . . 7 (𝑦 = dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂)))
61 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = dom 𝑂 → (𝑂𝑦) = (𝑂 dom 𝑂))
6261sseq2d 3774 . . . . . . . . . . 11 (𝑦 = dom 𝑂 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂 dom 𝑂)))
6362ifbid 4252 . . . . . . . . . 10 (𝑦 = dom 𝑂 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
6463mpteq2dv 4897 . . . . . . . . 9 (𝑦 = dom 𝑂 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
6564fveq2d 6356 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
66 suceq 5951 . . . . . . . . 9 (𝑦 = dom 𝑂 → suc 𝑦 = suc dom 𝑂)
6766fveq2d 6356 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc dom 𝑂))
6865, 67eleq12d 2833 . . . . . . 7 (𝑦 = dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
6960, 68imbi12d 333 . . . . . 6 (𝑦 = dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
7069imbi2d 329 . . . . 5 (𝑦 = dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))))
71 eleq1 2827 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72 sseq2 3768 . . . . . . . 8 (𝑦 = ∅ → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ ∅))
7371, 72anbi12d 749 . . . . . . 7 (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅)))
74 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑂𝑦) = (𝑂‘∅))
7574sseq2d 3774 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
7675ifbid 4252 . . . . . . . . . 10 (𝑦 = ∅ → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
7776mpteq2dv 4897 . . . . . . . . 9 (𝑦 = ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
7877fveq2d 6356 . . . . . . . 8 (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
79 suceq 5951 . . . . . . . . 9 (𝑦 = ∅ → suc 𝑦 = suc ∅)
8079fveq2d 6356 . . . . . . . 8 (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
8178, 80eleq12d 2833 . . . . . . 7 (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
8273, 81imbi12d 333 . . . . . 6 (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83 eleq1 2827 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂𝑢 ∈ dom 𝑂))
84 sseq2 3768 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ 𝑢))
8583, 84anbi12d 749 . . . . . . 7 (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)))
86 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑂𝑦) = (𝑂𝑢))
8786sseq2d 3774 . . . . . . . . . . 11 (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂𝑢)))
8887ifbid 4252 . . . . . . . . . 10 (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
8988mpteq2dv 4897 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
9089fveq2d 6356 . . . . . . . 8 (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))
91 suceq 5951 . . . . . . . . 9 (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
9291fveq2d 6356 . . . . . . . 8 (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
9390, 92eleq12d 2833 . . . . . . 7 (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
9485, 93imbi12d 333 . . . . . 6 (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95 eleq1 2827 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96 sseq2 3768 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ suc 𝑢))
9795, 96anbi12d 749 . . . . . . 7 (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢)))
98 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = suc 𝑢 → (𝑂𝑦) = (𝑂‘suc 𝑢))
9998sseq2d 3774 . . . . . . . . . . 11 (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
10099ifbid 4252 . . . . . . . . . 10 (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
101100mpteq2dv 4897 . . . . . . . . 9 (𝑦 = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
102101fveq2d 6356 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
103 suceq 5951 . . . . . . . . 9 (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104103fveq2d 6356 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105102, 104eleq12d 2833 . . . . . . 7 (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
10697, 105imbi12d 333 . . . . . 6 (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107 f1ocnvfv2 6696 . . . . . . . . . . . . 13 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
10848, 16, 107syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
109108sseq2d 3774 . . . . . . . . . . 11 (𝜑 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥𝑋))
110109ifbid 4252 . . . . . . . . . 10 (𝜑 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥𝑋, (𝐹𝑥), ∅))
111110mpteq2dv 4897 . . . . . . . . 9 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅)))
112111fveq2d 6356 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))))
113 cantnflem1.h . . . . . . . . 9 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐺‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 8758 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
115112, 114eqeltrd 2839 . . . . . . 7 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
116 ss0 4117 . . . . . . . . . . . . . 14 ((𝑂𝑋) ⊆ ∅ → (𝑂𝑋) = ∅)
117116fveq2d 6356 . . . . . . . . . . . . 13 ((𝑂𝑋) ⊆ ∅ → (𝑂‘(𝑂𝑋)) = (𝑂‘∅))
118117sseq2d 3774 . . . . . . . . . . . 12 ((𝑂𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119118ifbid 4252 . . . . . . . . . . 11 ((𝑂𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
120119mpteq2dv 4897 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
121120fveq2d 6356 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
122 suceq 5951 . . . . . . . . . . 11 ((𝑂𝑋) = ∅ → suc (𝑂𝑋) = suc ∅)
123116, 122syl 17 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → suc (𝑂𝑋) = suc ∅)
124123fveq2d 6356 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc ∅))
125121, 124eleq12d 2833 . . . . . . . 8 ((𝑂𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126125adantl 473 . . . . . . 7 ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127115, 126syl5ibcom 235 . . . . . 6 (𝜑 → ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128 ordelon 5908 . . . . . . . . . . . . 13 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
12936, 52, 128sylancr 698 . . . . . . . . . . . 12 (𝜑 → (𝑂𝑋) ∈ On)
130129adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
13136a1i 11 . . . . . . . . . . . 12 (𝜑 → Ord dom 𝑂)
132 ordelon 5908 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133131, 132sylan 489 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
134 onsseleq 5926 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
135130, 133, 134syl2anc 696 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
136 sucelon 7182 . . . . . . . . . . . . . . 15 (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
137133, 136sylibr 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
138 eloni 5894 . . . . . . . . . . . . . 14 (𝑢 ∈ On → Ord 𝑢)
139137, 138syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
140 ordsssuc 5973 . . . . . . . . . . . . 13 (((𝑂𝑋) ∈ On ∧ Ord 𝑢) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
141130, 139, 140syl2anc 696 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
142 ordtr 5898 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → Tr dom 𝑂)
14336, 142mp1i 13 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
144 simprl 811 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
145 trsuc 5971 . . . . . . . . . . . . . . . 16 ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
146143, 144, 145syl2anc 696 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
147 simprr 813 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ⊆ 𝑢)
148146, 147jca 555 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢))
1499adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
15010adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
151 oecl 7786 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
152149, 150, 151syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 𝐵) ∈ On)
1538, 149, 150cantnff 8744 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
1548, 9, 10cantnfs 8736 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
15512, 154mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
156155simpld 477 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝐵𝐴)
157156ffvelrnda 6522 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → (𝐹𝑥) ∈ 𝐴)
1588, 9, 10cantnfs 8736 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
15913, 158mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
160159simpld 477 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺:𝐵𝐴)
1618, 9, 10, 11, 12, 13, 14, 15oemapvali 8754 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑋𝐵 ∧ (𝐹𝑋) ∈ (𝐺𝑋) ∧ ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤))))
162161simp1d 1137 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
163160, 162ffvelrnd 6523 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐺𝑋) ∈ 𝐴)
164 ne0i 4064 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑋) ∈ 𝐴𝐴 ≠ ∅)
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ≠ ∅)
166 on0eln0 5941 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
1679, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∅ ∈ 𝐴𝐴 ≠ ∅))
168165, 167mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∅ ∈ 𝐴)
169168adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → ∅ ∈ 𝐴)
170157, 169ifcld 4275 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ 𝐴)
171 eqid 2760 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
172170, 171fmptd 6548 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴)
173 mptexg 6648 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ On → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
17410, 173syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
175 funmpt 6087 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
177155simprd 482 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 finSupp ∅)
178 eqid 2760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 supp ∅) = (𝐹 supp ∅)
179 eqimss2 3799 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 supp ∅) = (𝐹 supp ∅) → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
180178, 179mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
181 0ex 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∅ ∈ V)
183156, 180, 10, 182suppssr 7495 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑥) = ∅)
184183ifeq1d 4248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
185 ifid 4269 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑥 ⊆ (𝑂𝑢), ∅, ∅) = ∅
186184, 185syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
187186, 10suppss2 7498 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
188 fsuppsssupp 8456 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V ∧ Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
189174, 176, 177, 187, 188syl22anc 1478 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
1908, 9, 10cantnfs 8736 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴 ∧ (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)))
191172, 189, 190mpbir2and 995 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
192191adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
193153, 192ffvelrnd 6523 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵))
194 onelon 5909 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
195152, 193, 194syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
19631adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
197 elnn 7240 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
198144, 196, 197syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
199113cantnfvalf 8735 . . . . . . . . . . . . . . . . . . 19 𝐻:ω⟶On
200199ffvelrni 6521 . . . . . . . . . . . . . . . . . 18 (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
201198, 200syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
202 suppssdm 7476 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
203 fdm 6212 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
204160, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = 𝐵)
205202, 204syl5sseq 3794 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
206205adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
2072oif 8600 . . . . . . . . . . . . . . . . . . . . . . 23 𝑂:dom 𝑂⟶(𝐺 supp ∅)
208207ffvelrni 6521 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
209144, 208syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
210206, 209sseldd 3745 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
211 onelon 5909 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
212150, 210, 211syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
213 oecl 7786 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
214149, 212, 213syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
215156adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐹:𝐵𝐴)
216215, 210ffvelrnd 6523 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
217 onelon 5909 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
218149, 216, 217syl2anc 696 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
219 omcl 7785 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
220214, 218, 219syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
221 oaord 7796 . . . . . . . . . . . . . . . . 17 ((((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
222195, 201, 220, 221syl3anc 1477 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
223 ifeq1 4234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
224 ifid 4269 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
225223, 224syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = ∅)
226 ifeq1 4234 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅))
227 ifid 4269 . . . . . . . . . . . . . . . . . . . . . . 23 if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅) = ∅
228226, 227syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = ∅)
229225, 228eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) ↔ ∅ = ∅))
230 onss 7155 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → 𝐵 ⊆ On)
23110, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ⊆ On)
232231sselda 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐵) → 𝑥 ∈ On)
233232adantlr 753 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → 𝑥 ∈ On)
234212adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑂‘suc 𝑢) ∈ On)
235 onsseleq 5926 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
236233, 234, 235syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
237236adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
238233adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → 𝑥 ∈ On)
239207ffvelrni 6521 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ dom 𝑂 → (𝑂𝑢) ∈ (𝐺 supp ∅))
240146, 239syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝐺 supp ∅))
241206, 240sseldd 3745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ 𝐵)
242 onelon 5909 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ (𝑂𝑢) ∈ 𝐵) → (𝑂𝑢) ∈ On)
243150, 241, 242syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ On)
244243ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑂𝑢) ∈ On)
245 onsssuc 5974 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
246238, 244, 245syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
247 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑢 ∈ V
248247sucid 5965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ suc 𝑢
24946adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
250 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
251249, 146, 144, 250syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
252247sucex 7176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc 𝑢 ∈ V
253252epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 E suc 𝑢𝑢 ∈ suc 𝑢)
254 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑂‘suc 𝑢) ∈ V
255254epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
256251, 253, 2553bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢)))
257248, 256mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
258 eloni 5894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
259212, 258syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
260 ordelsuc 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑂𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
261243, 259, 260syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
262257, 261mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
263262ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
264263sseld 3743 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
265246, 264sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
266 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ 𝑥)
267249ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
268267, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
2698, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 8757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
270 f1ocnvfv2 6696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
271268, 269, 270syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂‘(𝑂𝑥)) = 𝑥)
272266, 271eleqtrrd 2842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
273146ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
274268, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
275274, 269ffvelrnd 6523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ dom 𝑂)
276 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
277267, 273, 275, 276syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
278 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂𝑥) ∈ V
279278epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 E (𝑂𝑥) ↔ 𝑢 ∈ (𝑂𝑥))
280 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂‘(𝑂𝑥)) ∈ V
281280epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑢) E (𝑂‘(𝑂𝑥)) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
282277, 279, 2813bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥))))
283272, 282mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ (𝑂𝑥))
284 ordelon 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂) → (𝑂𝑥) ∈ On)
28536, 275, 284sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ On)
286 eloni 5894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑥) ∈ On → Ord (𝑂𝑥))
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → Ord (𝑂𝑥))
288 ordelsuc 7185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢 ∈ (𝑂𝑥) ∧ Ord (𝑂𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
289283, 287, 288syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
290283, 289mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (𝑂𝑥))
291144ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
29236, 291, 132sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
293 ontri1 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc 𝑢 ∈ On ∧ (𝑂𝑥) ∈ On) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
294292, 285, 293syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
295290, 294mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ (𝑂𝑥) ∈ suc 𝑢)
296 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
297267, 275, 291, 296syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
298252epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑥) E suc 𝑢 ↔ (𝑂𝑥) ∈ suc 𝑢)
299254epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢))
300297, 298, 2993bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢)))
301271eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
302300, 301bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢𝑥 ∈ (𝑂‘suc 𝑢)))
303295, 302mtbid 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
304303expr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑂𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
305304con2d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂𝑢) ∈ 𝑥))
306 ontri1 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
307238, 244, 306syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
308305, 307sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂𝑢)))
309265, 308impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
310309orbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
311237, 310bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
312 orcom 401 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)))
313311, 312syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢))))
314313ifbid 4252 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
315 eqidd 2761 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ∅ = ∅)
316229, 314, 315pm2.61ne 3017 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
317316mpteq2dva 4896 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)))
318317fveq2d 6356 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))))
319 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑥) ∈ V
320319, 181ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
322321ralrimivw 3105 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
323171fnmpt 6181 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
325181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∅ ∈ V)
326 suppvalfn 7470 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅})
327 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝐵
328 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐵
329 nffvmpt1 6360 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)
330 nfcv 2902 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥
331329, 330nfne 3032 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅
332 nfv 1992 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅
333 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥))
334333neeq1d 2991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅))
335327, 328, 331, 332, 334cbvrab 3338 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅}
336326, 335syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
337324, 150, 325, 336syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
338 eqidd 2761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
339320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
340338, 339fvmpt2d 6455 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
341340neeq1d 2991 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
342339biantrurd 530 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)))
343 dif1o 7749 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
344342, 343syl6bbr 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)))
345341, 344bitrd 268 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)))
346345rabbidva 3328 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
347337, 346eqtrd 2794 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
348320, 343mpbiran 991 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)
349 ifeq1 4234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
350349, 185syl6eq 2810 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
351350necon3i 2964 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → (𝐹𝑥) ≠ ∅)
352 iffalse 4239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ⊆ (𝑂𝑢) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
353352necon1ai 2959 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂𝑢))
354351, 353jca 555 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → ((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)))
355265expimpd 630 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
356354, 355syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
357348, 356syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) → 𝑥 ∈ (𝑂‘suc 𝑢)))
3583573impia 1110 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵 ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
359358rabssdv 3823 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
360347, 359eqsstrd 3780 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
361 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
362 sseq1 3767 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑦 ⊆ (𝑂𝑢)))
363361, 362orbi12d 748 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢))))
364 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
365363, 364ifbieq1d 4253 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
366365cbvmptv 4902 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
367 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑂‘suc 𝑢) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
368367adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐵𝑦 = (𝑂‘suc 𝑢)) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
369368ifeq1da 4260 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
370362, 364ifbieq1d 4253 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
371 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑦) ∈ V
372371, 181ifex 4300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅) ∈ V
373370, 171, 372fvmpt 6444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
374373ifeq2d 4249 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅)))
375 ifor 4279 . . . . . . . . . . . . . . . . . . . . . . . 24 if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
376374, 375syl6eqr 2812 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
377369, 376eqtr3d 2796 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
378377mpteq2ia 4892 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦))) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
379366, 378eqtr4i 2785 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
3808, 149, 150, 192, 210, 216, 360, 379cantnfp1 8751 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))))
381380simprd 482 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
382318, 381eqtrd 2794 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
3838, 9, 10, 2, 13, 113cantnfsuc 8740 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
384198, 383syldan 488 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
385161simp3d 1139 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
386385adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
387108adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) = 𝑋)
388129adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ On)
389137adantrr 755 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
390 onsssuc 5974 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑂𝑋) ∈ On ∧ 𝑢 ∈ On) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
391388, 389, 390syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
392147, 391mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ suc 𝑢)
39352adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ dom 𝑂)
394 isorel 6739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
395249, 393, 144, 394syl12anc 1475 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
396252epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂𝑋) E suc 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢)
397254epelc 5181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
398395, 396, 3973bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢)))
399392, 398mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
400387, 399eqeltrrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
401 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → (𝑋𝑤𝑋 ∈ (𝑂‘suc 𝑢)))
402 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐹𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
403 fveq2 6352 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐺𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
404402, 403eqeq12d 2775 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
405401, 404imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑂‘suc 𝑢) → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
406405rspcv 3445 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
407210, 386, 400, 406syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
408407oveq2d 6829 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
409408oveq1d 6828 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
410384, 409eqtr4d 2797 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
411382, 410eleq12d 2833 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
412222, 411bitr4d 271 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
413412biimpd 219 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
414148, 413embantd 59 . . . . . . . . . . . . 13 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
415414expr 644 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
416141, 415sylbird 250 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
417 fveq2 6352 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑋) = suc 𝑢 → (𝑂‘(𝑂𝑋)) = (𝑂‘suc 𝑢))
418417sseq2d 3774 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
419418ifbid 4252 . . . . . . . . . . . . . . . . 17 ((𝑂𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
420419mpteq2dv 4897 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
421420fveq2d 6356 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
422 suceq 5951 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → suc (𝑂𝑋) = suc suc 𝑢)
423422fveq2d 6356 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc suc 𝑢))
424421, 423eleq12d 2833 . . . . . . . . . . . . . 14 ((𝑂𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
425115, 424syl5ibcom 235 . . . . . . . . . . . . 13 (𝜑 → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
426425adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
427426a1dd 50 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
428416, 427jaod 394 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
429135, 428sylbid 230 . . . . . . . . 9 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
430429expimpd 630 . . . . . . . 8 (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
431430com23 86 . . . . . . 7 (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
432431a1i 11 . . . . . 6 (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
43382, 94, 106, 127, 432finds2 7259 . . . . 5 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
43470, 433vtoclga 3412 . . . 4 ( dom 𝑂 ∈ ω → (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
43557, 434mpcom 38 . . 3 (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
43644, 54, 435mp2and 717 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))
437156feqmptd 6411 . . . 4 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
438 eqeq2 2771 . . . . . 6 ((𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = (𝐹𝑥) ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
439 eqeq2 2771 . . . . . 6 (∅ = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = ∅ ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
440 eqidd 2761 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = (𝐹𝑥))
441207ffvelrni 6521 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
44244, 441syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
443205, 442sseldd 3745 . . . . . . . . . . . 12 (𝜑 → (𝑂 dom 𝑂) ∈ 𝐵)
444 onelon 5909 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑂 dom 𝑂) ∈ 𝐵) → (𝑂 dom 𝑂) ∈ On)
44510, 443, 444syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) ∈ On)
446445adantr 472 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑂 dom 𝑂) ∈ On)
447 ontri1 5918 . . . . . . . . . 10 ((𝑥 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
448232, 446, 447syl2anc 696 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
449448con2bid 343 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)))
450 simprl 811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥𝐵)
451385adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
452 eloni 5894 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) ∈ On → Ord (𝑂𝑋))
453129, 452syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord (𝑂𝑋))
454 orduni 7159 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑂 → Ord dom 𝑂)
45536, 454ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord dom 𝑂
456 ordtri1 5917 . . . . . . . . . . . . . . . . 17 ((Ord (𝑂𝑋) ∧ Ord dom 𝑂) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
457453, 455, 456sylancl 697 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
45854, 457mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
459 isorel 6739 . . . . . . . . . . . . . . . . . 18 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
46046, 44, 52, 459syl12anc 1475 . . . . . . . . . . . . . . . . 17 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
461 fvex 6362 . . . . . . . . . . . . . . . . . 18 (𝑂𝑋) ∈ V
462461epelc 5181 . . . . . . . . . . . . . . . . 17 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
463 fvex 6362 . . . . . . . . . . . . . . . . . 18 (𝑂‘(𝑂𝑋)) ∈ V
464463epelc 5181 . . . . . . . . . . . . . . . . 17 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
465460, 462, 4643bitr3g 302 . . . . . . . . . . . . . . . 16 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
466108eleq2d 2825 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
467465, 466bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
468458, 467mtbid 313 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
469 onelon 5909 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
47010, 162, 469syl2anc 696 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ On)
471 ontri1 5918 . . . . . . . . . . . . . . 15 ((𝑋 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
472470, 445, 471syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
473468, 472mpbird 247 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (𝑂 dom 𝑂))
474473adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂 dom 𝑂))
475 simprr 813 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝑂 dom 𝑂) ∈ 𝑥)
476470adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
477232adantrr 755 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
478 ontr2 5933 . . . . . . . . . . . . 13 ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
479476, 477, 478syl2anc 696 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
480474, 475, 479mp2and 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋𝑥)
481 eleq2 2828 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑋𝑤𝑋𝑥))
482 fveq2 6352 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
483 fveq2 6352 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐺𝑤) = (𝐺𝑥))
484482, 483eqeq12d 2775 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹𝑥) = (𝐺𝑥)))
485481, 484imbi12d 333 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
486485rspcv 3445 . . . . . . . . . . 11 (𝑥𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
487450, 451, 480, 486syl3c 66 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = (𝐺𝑥))
488475adantr 472 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂 dom 𝑂) ∈ 𝑥)
48946ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
49044ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ dom 𝑂)
49151ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
492 ffvelrn 6520 . . . . . . . . . . . . . . . . . 18 ((𝑂:(𝐺 supp ∅)⟶dom 𝑂𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
493491, 492sylancom 704 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
494 isorel 6739 . . . . . . . . . . . . . . . . 17 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
495489, 490, 493, 494syl12anc 1475 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
496278epelc 5181 . . . . . . . . . . . . . . . 16 ( dom 𝑂 E (𝑂𝑥) ↔ dom 𝑂 ∈ (𝑂𝑥))
497280epelc 5181 . . . . . . . . . . . . . . . 16 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)))
498495, 496, 4973bitr3g 302 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥))))
49948ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
500499, 270sylancom 704 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
501500eleq2d 2825 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
502498, 501bitrd 268 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
503488, 502mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ (𝑂𝑥))
504 elssuni 4619 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∈ dom 𝑂 → (𝑂𝑥) ⊆ dom 𝑂)
505493, 504syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ⊆ dom 𝑂)
50636, 493, 284sylancr 698 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ On)
507506, 286syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (𝑂𝑥))
508 ordtri1 5917 . . . . . . . . . . . . . . 15 ((Ord (𝑂𝑥) ∧ Ord dom 𝑂) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
509507, 455, 508sylancl 697 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
510505, 509mpbid 222 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ dom 𝑂 ∈ (𝑂𝑥))
511503, 510pm2.65da 601 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
512450, 511eldifd 3726 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
513 ssid 3765 . . . . . . . . . . . . 13 (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
514513a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
515160, 514, 10, 182suppssr 7495 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑥) = ∅)
516512, 515syldan 488 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐺𝑥) = ∅)
517487, 516eqtrd 2794 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = ∅)
518517expr 644 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 → (𝐹𝑥) = ∅))
519449, 518sylbird 250 . . . . . . 7 ((𝜑𝑥𝐵) → (¬ 𝑥 ⊆ (𝑂 dom 𝑂) → (𝐹𝑥) = ∅))
520519imp 444 . . . . . 6 (((𝜑𝑥𝐵) ∧ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = ∅)
521438, 439, 440, 520ifbothda 4267 . . . . 5 ((𝜑𝑥𝐵) → (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
522521mpteq2dva 4896 . . . 4 (𝜑 → (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
523437, 522eqtrd 2794 . . 3 (𝜑𝐹 = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
524523fveq2d 6356 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
5258, 9, 10, 2, 13, 113cantnfval 8738 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
52643fveq2d 6356 . . 3 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
527525, 526eqtrd 2794 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc dom 𝑂))
528436, 524, 5273eltr4d 2854 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  cdif 3712  wss 3715  c0 4058  ifcif 4230   cuni 4588   class class class wbr 4804  {copab 4864  cmpt 4881  Tr wtr 4904   E cep 5178   We wwe 5224  ccnv 5265  dom cdm 5266  Ord word 5883  Oncon0 5884  Lim wlim 5885  suc csuc 5886  Fun wfun 6043   Fn wfn 6044  wf 6045  1-1-ontowf1o 6048  cfv 6049   Isom wiso 6050  (class class class)co 6813  cmpt2 6815  ωcom 7230   supp csupp 7463  seq𝜔cseqom 7711  1𝑜c1o 7722   +𝑜 coa 7726   ·𝑜 comu 7727  𝑜 coe 7728  cen 8118   finSupp cfsupp 8440  OrdIsocoi 8579   CNF ccnf 8731
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-seqom 7712  df-1o 7729  df-2o 7730  df-oadd 7733  df-omul 7734  df-oexp 7735  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-oi 8580  df-cnf 8732
This theorem is referenced by:  cantnf  8763
  Copyright terms: Public domain W3C validator