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

Theorem cantnflem1 8624
Description: Lemma for cantnf 8628. 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 6718 . . . . . 6 (𝐺 supp ∅) ∈ V
2 cantnflem1.o . . . . . . 7 𝑂 = OrdIso( E , (𝐺 supp ∅))
32oion 8482 . . . . . 6 ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
41, 3mp1i 13 . . . . 5 (𝜑 → dom 𝑂 ∈ On)
5 uniexg 6997 . . . . 5 (dom 𝑂 ∈ On → dom 𝑂 ∈ V)
6 sucidg 5841 . . . . 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 8620 . . . . . . . . 9 (𝜑𝑋 ∈ (𝐺 supp ∅))
17 n0i 3953 . . . . . . . . 9 (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19 ovexd 6720 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) ∈ V)
208, 9, 10, 2, 13cantnfcl 8602 . . . . . . . . . . 11 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
2120simpld 474 . . . . . . . . . 10 (𝜑 → E We (𝐺 supp ∅))
222oien 8484 . . . . . . . . . 10 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
2319, 21, 22syl2anc 694 . . . . . . . . 9 (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24 breq1 4688 . . . . . . . . . 10 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25 ensymb 8045 . . . . . . . . . . 11 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26 en0 8060 . . . . . . . . . . 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 478 . . . . . . . 8 (𝜑 → dom 𝑂 ∈ ω)
32 nnlim 7120 . . . . . . . 8 (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
3331, 32syl 17 . . . . . . 7 (𝜑 → ¬ Lim dom 𝑂)
34 ioran 510 . . . . . . 7 (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
3530, 33, 34sylanbrc 699 . . . . . 6 (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
362oicl 8475 . . . . . . 7 Ord dom 𝑂
37 unizlim 5882 . . . . . . 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 7072 . . . . . . 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 2733 . . 3 (𝜑 dom 𝑂 ∈ dom 𝑂)
452oiiso 8483 . . . . . . . 8 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
4619, 21, 45syl2anc 694 . . . . . . 7 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47 isof1o 6613 . . . . . . 7 (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
4846, 47syl 17 . . . . . 6 (𝜑𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
49 f1ocnv 6187 . . . . . 6 (𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) → 𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50 f1of 6175 . . . . . 6 (𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5148, 49, 503syl 18 . . . . 5 (𝜑𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5251, 16ffvelrnd 6400 . . . 4 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
53 elssuni 4499 . . . 4 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5452, 53syl 17 . . 3 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
5543, 31eqeltrrd 2731 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
56 peano2b 7123 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
5755, 56sylibr 224 . . . 4 (𝜑 dom 𝑂 ∈ ω)
58 eleq1 2718 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝑦 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
59 sseq2 3660 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ dom 𝑂))
6058, 59anbi12d 747 . . . . . . 7 (𝑦 = dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂)))
61 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = dom 𝑂 → (𝑂𝑦) = (𝑂 dom 𝑂))
6261sseq2d 3666 . . . . . . . . . . 11 (𝑦 = dom 𝑂 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂 dom 𝑂)))
6362ifbid 4141 . . . . . . . . . 10 (𝑦 = dom 𝑂 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
6463mpteq2dv 4778 . . . . . . . . 9 (𝑦 = dom 𝑂 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
6564fveq2d 6233 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
66 suceq 5828 . . . . . . . . 9 (𝑦 = dom 𝑂 → suc 𝑦 = suc dom 𝑂)
6766fveq2d 6233 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc dom 𝑂))
6865, 67eleq12d 2724 . . . . . . 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 2718 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72 sseq2 3660 . . . . . . . 8 (𝑦 = ∅ → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ ∅))
7371, 72anbi12d 747 . . . . . . 7 (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅)))
74 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑂𝑦) = (𝑂‘∅))
7574sseq2d 3666 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
7675ifbid 4141 . . . . . . . . . 10 (𝑦 = ∅ → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
7776mpteq2dv 4778 . . . . . . . . 9 (𝑦 = ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
7877fveq2d 6233 . . . . . . . 8 (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
79 suceq 5828 . . . . . . . . 9 (𝑦 = ∅ → suc 𝑦 = suc ∅)
8079fveq2d 6233 . . . . . . . 8 (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
8178, 80eleq12d 2724 . . . . . . 7 (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
8273, 81imbi12d 333 . . . . . 6 (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83 eleq1 2718 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂𝑢 ∈ dom 𝑂))
84 sseq2 3660 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ 𝑢))
8583, 84anbi12d 747 . . . . . . 7 (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)))
86 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑂𝑦) = (𝑂𝑢))
8786sseq2d 3666 . . . . . . . . . . 11 (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂𝑢)))
8887ifbid 4141 . . . . . . . . . 10 (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
8988mpteq2dv 4778 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
9089fveq2d 6233 . . . . . . . 8 (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))
91 suceq 5828 . . . . . . . . 9 (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
9291fveq2d 6233 . . . . . . . 8 (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
9390, 92eleq12d 2724 . . . . . . 7 (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
9485, 93imbi12d 333 . . . . . 6 (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95 eleq1 2718 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96 sseq2 3660 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ suc 𝑢))
9795, 96anbi12d 747 . . . . . . 7 (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢)))
98 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = suc 𝑢 → (𝑂𝑦) = (𝑂‘suc 𝑢))
9998sseq2d 3666 . . . . . . . . . . 11 (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
10099ifbid 4141 . . . . . . . . . 10 (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
101100mpteq2dv 4778 . . . . . . . . 9 (𝑦 = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
102101fveq2d 6233 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
103 suceq 5828 . . . . . . . . 9 (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104103fveq2d 6233 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105102, 104eleq12d 2724 . . . . . . 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 6573 . . . . . . . . . . . . 13 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
10848, 16, 107syl2anc 694 . . . . . . . . . . . 12 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
109108sseq2d 3666 . . . . . . . . . . 11 (𝜑 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥𝑋))
110109ifbid 4141 . . . . . . . . . 10 (𝜑 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥𝑋, (𝐹𝑥), ∅))
111110mpteq2dv 4778 . . . . . . . . 9 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅)))
112111fveq2d 6233 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))))
113 cantnflem1.h . . . . . . . . 9 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐺‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 8623 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
115112, 114eqeltrd 2730 . . . . . . 7 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
116 ss0 4007 . . . . . . . . . . . . . 14 ((𝑂𝑋) ⊆ ∅ → (𝑂𝑋) = ∅)
117116fveq2d 6233 . . . . . . . . . . . . 13 ((𝑂𝑋) ⊆ ∅ → (𝑂‘(𝑂𝑋)) = (𝑂‘∅))
118117sseq2d 3666 . . . . . . . . . . . 12 ((𝑂𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119118ifbid 4141 . . . . . . . . . . 11 ((𝑂𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
120119mpteq2dv 4778 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
121120fveq2d 6233 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
122 suceq 5828 . . . . . . . . . . 11 ((𝑂𝑋) = ∅ → suc (𝑂𝑋) = suc ∅)
123116, 122syl 17 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → suc (𝑂𝑋) = suc ∅)
124123fveq2d 6233 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc ∅))
125121, 124eleq12d 2724 . . . . . . . 8 ((𝑂𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126125adantl 481 . . . . . . 7 ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127115, 126syl5ibcom 235 . . . . . 6 (𝜑 → ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128 ordelon 5785 . . . . . . . . . . . . 13 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
12936, 52, 128sylancr 696 . . . . . . . . . . . 12 (𝜑 → (𝑂𝑋) ∈ On)
130129adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
13136a1i 11 . . . . . . . . . . . 12 (𝜑 → Ord dom 𝑂)
132 ordelon 5785 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133131, 132sylan 487 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
134 onsseleq 5803 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
135130, 133, 134syl2anc 694 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
136 sucelon 7059 . . . . . . . . . . . . . . 15 (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
137133, 136sylibr 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
138 eloni 5771 . . . . . . . . . . . . . 14 (𝑢 ∈ On → Ord 𝑢)
139137, 138syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
140 ordsssuc 5850 . . . . . . . . . . . . 13 (((𝑂𝑋) ∈ On ∧ Ord 𝑢) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
141130, 139, 140syl2anc 694 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
142 ordtr 5775 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → Tr dom 𝑂)
14336, 142mp1i 13 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
144 simprl 809 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
145 trsuc 5848 . . . . . . . . . . . . . . . 16 ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
146143, 144, 145syl2anc 694 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
147 simprr 811 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ⊆ 𝑢)
148146, 147jca 553 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢))
1499adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
15010adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
151 oecl 7662 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
152149, 150, 151syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 𝐵) ∈ On)
1538, 149, 150cantnff 8609 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
1548, 9, 10cantnfs 8601 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
15512, 154mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
156155simpld 474 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝐵𝐴)
157156ffvelrnda 6399 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → (𝐹𝑥) ∈ 𝐴)
1588, 9, 10cantnfs 8601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
15913, 158mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
160159simpld 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺:𝐵𝐴)
1618, 9, 10, 11, 12, 13, 14, 15oemapvali 8619 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑋𝐵 ∧ (𝐹𝑋) ∈ (𝐺𝑋) ∧ ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤))))
162161simp1d 1093 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
163160, 162ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐺𝑋) ∈ 𝐴)
164 ne0i 3954 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑋) ∈ 𝐴𝐴 ≠ ∅)
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ≠ ∅)
166 on0eln0 5818 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
1679, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∅ ∈ 𝐴𝐴 ≠ ∅))
168165, 167mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∅ ∈ 𝐴)
169168adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → ∅ ∈ 𝐴)
170157, 169ifcld 4164 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ 𝐴)
171 eqid 2651 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
172170, 171fmptd 6425 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴)
173 mptexg 6525 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ On → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
17410, 173syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
175 funmpt 5964 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
177155simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 finSupp ∅)
178 eqid 2651 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 supp ∅) = (𝐹 supp ∅)
179 eqimss2 3691 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 supp ∅) = (𝐹 supp ∅) → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
180178, 179mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
181 0ex 4823 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∅ ∈ V)
183156, 180, 10, 182suppssr 7371 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑥) = ∅)
184183ifeq1d 4137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
185 ifid 4158 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑥 ⊆ (𝑂𝑢), ∅, ∅) = ∅
186184, 185syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
187186, 10suppss2 7374 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
188 fsuppsssupp 8332 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V ∧ Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
189174, 176, 177, 187, 188syl22anc 1367 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
1908, 9, 10cantnfs 8601 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴 ∧ (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)))
191172, 189, 190mpbir2and 977 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
192191adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
193153, 192ffvelrnd 6400 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵))
194 onelon 5786 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
195152, 193, 194syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
19631adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
197 elnn 7117 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
198144, 196, 197syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
199113cantnfvalf 8600 . . . . . . . . . . . . . . . . . . 19 𝐻:ω⟶On
200199ffvelrni 6398 . . . . . . . . . . . . . . . . . 18 (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
201198, 200syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
202 suppssdm 7353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
203 fdm 6089 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
204160, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = 𝐵)
205202, 204syl5sseq 3686 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
206205adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
2072oif 8476 . . . . . . . . . . . . . . . . . . . . . . 23 𝑂:dom 𝑂⟶(𝐺 supp ∅)
208207ffvelrni 6398 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
209144, 208syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
210206, 209sseldd 3637 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
211 onelon 5786 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
212150, 210, 211syl2anc 694 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
213 oecl 7662 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
214149, 212, 213syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
215156adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐹:𝐵𝐴)
216215, 210ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
217 onelon 5786 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
218149, 216, 217syl2anc 694 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
219 omcl 7661 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
220214, 218, 219syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
221 oaord 7672 . . . . . . . . . . . . . . . . 17 ((((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
222195, 201, 220, 221syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
223 ifeq1 4123 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
224 ifid 4158 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
225223, 224syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = ∅)
226 ifeq1 4123 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅))
227 ifid 4158 . . . . . . . . . . . . . . . . . . . . . . 23 if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅) = ∅
228226, 227syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = ∅)
229225, 228eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) ↔ ∅ = ∅))
230 onss 7032 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → 𝐵 ⊆ On)
23110, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ⊆ On)
232231sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐵) → 𝑥 ∈ On)
233232adantlr 751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → 𝑥 ∈ On)
234212adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑂‘suc 𝑢) ∈ On)
235 onsseleq 5803 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
236233, 234, 235syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
237236adantr 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
238233adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → 𝑥 ∈ On)
239207ffvelrni 6398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ dom 𝑂 → (𝑂𝑢) ∈ (𝐺 supp ∅))
240146, 239syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝐺 supp ∅))
241206, 240sseldd 3637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ 𝐵)
242 onelon 5786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ (𝑂𝑢) ∈ 𝐵) → (𝑂𝑢) ∈ On)
243150, 241, 242syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ On)
244243ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑂𝑢) ∈ On)
245 onsssuc 5851 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
246238, 244, 245syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
247 vex 3234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑢 ∈ V
248247sucid 5842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ suc 𝑢
24946adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
250 isorel 6616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
251249, 146, 144, 250syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
252247sucex 7053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc 𝑢 ∈ V
253252epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 E suc 𝑢𝑢 ∈ suc 𝑢)
254 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑂‘suc 𝑢) ∈ V
255254epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
256251, 253, 2553bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢)))
257248, 256mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
258 eloni 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
259212, 258syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
260 ordelsuc 7062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑂𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
261243, 259, 260syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
262257, 261mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
263262ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
264263sseld 3635 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
265246, 264sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
266 simprr 811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ 𝑥)
267249ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
270 f1ocnvfv2 6573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
271268, 269, 270syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂‘(𝑂𝑥)) = 𝑥)
272266, 271eleqtrrd 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
273146ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
274268, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
275274, 269ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ dom 𝑂)
276 isorel 6616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
277267, 273, 275, 276syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
278 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂𝑥) ∈ V
279278epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 E (𝑂𝑥) ↔ 𝑢 ∈ (𝑂𝑥))
280 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂‘(𝑂𝑥)) ∈ V
281280epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑢) E (𝑂‘(𝑂𝑥)) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
282277, 279, 2813bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥))))
283272, 282mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ (𝑂𝑥))
284 ordelon 5785 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂) → (𝑂𝑥) ∈ On)
28536, 275, 284sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ On)
286 eloni 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑥) ∈ On → Ord (𝑂𝑥))
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → Ord (𝑂𝑥))
288 ordelsuc 7062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢 ∈ (𝑂𝑥) ∧ Ord (𝑂𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
289283, 287, 288syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
290283, 289mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (𝑂𝑥))
291144ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
29236, 291, 132sylancr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
293 ontri1 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc 𝑢 ∈ On ∧ (𝑂𝑥) ∈ On) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
294292, 285, 293syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
295290, 294mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ (𝑂𝑥) ∈ suc 𝑢)
296 isorel 6616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
297267, 275, 291, 296syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
298252epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑥) E suc 𝑢 ↔ (𝑂𝑥) ∈ suc 𝑢)
299254epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢))
300297, 298, 2993bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢)))
301271eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
302300, 301bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢𝑥 ∈ (𝑂‘suc 𝑢)))
303295, 302mtbid 313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
304303expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑂𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
305304con2d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂𝑢) ∈ 𝑥))
306 ontri1 5795 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
307238, 244, 306syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
308305, 307sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂𝑢)))
309265, 308impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
310309orbi1d 739 . . . . . . . . . . . . . . . . . . . . . . . 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 4141 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
315 eqidd 2652 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ∅ = ∅)
316229, 314, 315pm2.61ne 2908 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
317316mpteq2dva 4777 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)))
318317fveq2d 6233 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))))
319 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑥) ∈ V
320319, 181ifex 4189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
322321ralrimivw 2996 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
323171fnmpt 6058 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
325181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∅ ∈ V)
326 suppvalfn 7347 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅})
327 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝐵
328 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐵
329 nffvmpt1 6237 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)
330 nfcv 2793 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥
331329, 330nfne 2923 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅
332 nfv 1883 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅
333 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥))
334333neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅))
335327, 328, 331, 332, 334cbvrab 3229 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅}
336326, 335syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
337324, 150, 325, 336syl3anc 1366 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
338 eqidd 2652 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
339320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
340338, 339fvmpt2d 6332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
341340neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
342339biantrurd 528 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)))
343 dif1o 7625 . . . . . . . . . . . . . . . . . . . . . . . . 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 3219 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
347337, 346eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
348320, 343mpbiran 973 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)
349 ifeq1 4123 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
350349, 185syl6eq 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
351350necon3i 2855 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → (𝐹𝑥) ≠ ∅)
352 iffalse 4128 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ⊆ (𝑂𝑢) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
353352necon1ai 2850 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂𝑢))
354351, 353jca 553 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → ((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)))
355265expimpd 628 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
356354, 355syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
357348, 356syl5bi 232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) → 𝑥 ∈ (𝑂‘suc 𝑢)))
3583573impia 1280 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵 ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
359358rabssdv 3715 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
360347, 359eqsstrd 3672 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
361 eqeq1 2655 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
362 sseq1 3659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑦 ⊆ (𝑂𝑢)))
363361, 362orbi12d 746 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢))))
364 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
365363, 364ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
366365cbvmptv 4783 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
367 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑂‘suc 𝑢) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
368367adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐵𝑦 = (𝑂‘suc 𝑢)) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
369368ifeq1da 4149 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
370362, 364ifbieq1d 4142 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
371 fvex 6239 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑦) ∈ V
372371, 181ifex 4189 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅) ∈ V
373370, 171, 372fvmpt 6321 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
374373ifeq2d 4138 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅)))
375 ifor 4168 . . . . . . . . . . . . . . . . . . . . . . . 24 if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
376374, 375syl6eqr 2703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
377369, 376eqtr3d 2687 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
378377mpteq2ia 4773 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦))) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
379366, 378eqtr4i 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
3808, 149, 150, 192, 210, 216, 360, 379cantnfp1 8616 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))))
381380simprd 478 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
382318, 381eqtrd 2685 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
3838, 9, 10, 2, 13, 113cantnfsuc 8605 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
384198, 383syldan 486 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
385161simp3d 1095 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
386385adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
387108adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) = 𝑋)
388129adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ On)
389137adantrr 753 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
390 onsssuc 5851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑂𝑋) ∈ On ∧ 𝑢 ∈ On) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
391388, 389, 390syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
392147, 391mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ suc 𝑢)
39352adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ dom 𝑂)
394 isorel 6616 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
395249, 393, 144, 394syl12anc 1364 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
396252epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂𝑋) E suc 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢)
397254epelc 5060 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
398395, 396, 3973bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢)))
399392, 398mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
400387, 399eqeltrrd 2731 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
401 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → (𝑋𝑤𝑋 ∈ (𝑂‘suc 𝑢)))
402 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐹𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
403 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐺𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
404402, 403eqeq12d 2666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
405401, 404imbi12d 333 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑂‘suc 𝑢) → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
406405rspcv 3336 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
407210, 386, 400, 406syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
408407oveq2d 6706 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
409408oveq1d 6705 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
410384, 409eqtr4d 2688 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
411382, 410eleq12d 2724 . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . 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 6229 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑋) = suc 𝑢 → (𝑂‘(𝑂𝑋)) = (𝑂‘suc 𝑢))
418417sseq2d 3666 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
419418ifbid 4141 . . . . . . . . . . . . . . . . 17 ((𝑂𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
420419mpteq2dv 4778 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
421420fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
422 suceq 5828 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → suc (𝑂𝑋) = suc suc 𝑢)
423422fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc suc 𝑢))
424421, 423eleq12d 2724 . . . . . . . . . . . . . 14 ((𝑂𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
425115, 424syl5ibcom 235 . . . . . . . . . . . . 13 (𝜑 → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
426425adantr 480 . . . . . . . . . . . 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 628 . . . . . . . 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 7136 . . . . 5 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
43470, 433vtoclga 3303 . . . 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 715 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))
437156feqmptd 6288 . . . 4 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
438 eqeq2 2662 . . . . . 6 ((𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = (𝐹𝑥) ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
439 eqeq2 2662 . . . . . 6 (∅ = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = ∅ ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
440 eqidd 2652 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = (𝐹𝑥))
441207ffvelrni 6398 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
44244, 441syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
443205, 442sseldd 3637 . . . . . . . . . . . 12 (𝜑 → (𝑂 dom 𝑂) ∈ 𝐵)
444 onelon 5786 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑂 dom 𝑂) ∈ 𝐵) → (𝑂 dom 𝑂) ∈ On)
44510, 443, 444syl2anc 694 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) ∈ On)
446445adantr 480 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑂 dom 𝑂) ∈ On)
447 ontri1 5795 . . . . . . . . . 10 ((𝑥 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
448232, 446, 447syl2anc 694 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
449448con2bid 343 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)))
450 simprl 809 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥𝐵)
451385adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
452 eloni 5771 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) ∈ On → Ord (𝑂𝑋))
453129, 452syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord (𝑂𝑋))
454 orduni 7036 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑂 → Ord dom 𝑂)
45536, 454ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord dom 𝑂
456 ordtri1 5794 . . . . . . . . . . . . . . . . 17 ((Ord (𝑂𝑋) ∧ Ord dom 𝑂) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
457453, 455, 456sylancl 695 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
45854, 457mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
459 isorel 6616 . . . . . . . . . . . . . . . . . 18 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
46046, 44, 52, 459syl12anc 1364 . . . . . . . . . . . . . . . . 17 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
461 fvex 6239 . . . . . . . . . . . . . . . . . 18 (𝑂𝑋) ∈ V
462461epelc 5060 . . . . . . . . . . . . . . . . 17 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
463 fvex 6239 . . . . . . . . . . . . . . . . . 18 (𝑂‘(𝑂𝑋)) ∈ V
464463epelc 5060 . . . . . . . . . . . . . . . . 17 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
465460, 462, 4643bitr3g 302 . . . . . . . . . . . . . . . 16 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
466108eleq2d 2716 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
467465, 466bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
468458, 467mtbid 313 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
469 onelon 5786 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
47010, 162, 469syl2anc 694 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ On)
471 ontri1 5795 . . . . . . . . . . . . . . 15 ((𝑋 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
472470, 445, 471syl2anc 694 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
473468, 472mpbird 247 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (𝑂 dom 𝑂))
474473adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂 dom 𝑂))
475 simprr 811 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝑂 dom 𝑂) ∈ 𝑥)
476470adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
477232adantrr 753 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
478 ontr2 5810 . . . . . . . . . . . . 13 ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
479476, 477, 478syl2anc 694 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
480474, 475, 479mp2and 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋𝑥)
481 eleq2 2719 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑋𝑤𝑋𝑥))
482 fveq2 6229 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
483 fveq2 6229 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐺𝑤) = (𝐺𝑥))
484482, 483eqeq12d 2666 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹𝑥) = (𝐺𝑥)))
485481, 484imbi12d 333 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
486485rspcv 3336 . . . . . . . . . . 11 (𝑥𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
487450, 451, 480, 486syl3c 66 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = (𝐺𝑥))
488475adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂 dom 𝑂) ∈ 𝑥)
48946ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
49044ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ dom 𝑂)
49151ad2antrr 762 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
492 ffvelrn 6397 . . . . . . . . . . . . . . . . . 18 ((𝑂:(𝐺 supp ∅)⟶dom 𝑂𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
493491, 492sylancom 702 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
494 isorel 6616 . . . . . . . . . . . . . . . . 17 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
495489, 490, 493, 494syl12anc 1364 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
496278epelc 5060 . . . . . . . . . . . . . . . 16 ( dom 𝑂 E (𝑂𝑥) ↔ dom 𝑂 ∈ (𝑂𝑥))
497280epelc 5060 . . . . . . . . . . . . . . . 16 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)))
498495, 496, 4973bitr3g 302 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥))))
49948ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
500499, 270sylancom 702 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
501500eleq2d 2716 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
502498, 501bitrd 268 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
503488, 502mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ (𝑂𝑥))
504 elssuni 4499 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∈ dom 𝑂 → (𝑂𝑥) ⊆ dom 𝑂)
505493, 504syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ⊆ dom 𝑂)
50636, 493, 284sylancr 696 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ On)
507506, 286syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (𝑂𝑥))
508 ordtri1 5794 . . . . . . . . . . . . . . 15 ((Ord (𝑂𝑥) ∧ Ord dom 𝑂) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
509507, 455, 508sylancl 695 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
510505, 509mpbid 222 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ dom 𝑂 ∈ (𝑂𝑥))
511503, 510pm2.65da 599 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
512450, 511eldifd 3618 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
513 ssid 3657 . . . . . . . . . . . . 13 (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
514513a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
515160, 514, 10, 182suppssr 7371 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑥) = ∅)
516512, 515syldan 486 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐺𝑥) = ∅)
517487, 516eqtrd 2685 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = ∅)
518517expr 642 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 → (𝐹𝑥) = ∅))
519449, 518sylbird 250 . . . . . . 7 ((𝜑𝑥𝐵) → (¬ 𝑥 ⊆ (𝑂 dom 𝑂) → (𝐹𝑥) = ∅))
520519imp 444 . . . . . 6 (((𝜑𝑥𝐵) ∧ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = ∅)
521438, 439, 440, 520ifbothda 4156 . . . . 5 ((𝜑𝑥𝐵) → (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
522521mpteq2dva 4777 . . . 4 (𝜑 → (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
523437, 522eqtrd 2685 . . 3 (𝜑𝐹 = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
524523fveq2d 6233 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
5258, 9, 10, 2, 13, 113cantnfval 8603 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
52643fveq2d 6233 . . 3 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
527525, 526eqtrd 2685 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc dom 𝑂))
528436, 524, 5273eltr4d 2745 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  wss 3607  c0 3948  ifcif 4119   cuni 4468   class class class wbr 4685  {copab 4745  cmpt 4762  Tr wtr 4785   E cep 5057   We wwe 5101  ccnv 5142  dom cdm 5143  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  (class class class)co 6690  cmpt2 6692  ωcom 7107   supp csupp 7340  seq𝜔cseqom 7587  1𝑜c1o 7598   +𝑜 coa 7602   ·𝑜 comu 7603  𝑜 coe 7604  cen 7994   finSupp cfsupp 8316  OrdIsocoi 8455   CNF ccnf 8596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-seqom 7588  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-oexp 7611  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-oi 8456  df-cnf 8597
This theorem is referenced by:  cantnf  8628
  Copyright terms: Public domain W3C validator