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

Theorem cantnflem1 8546
Description: Lemma for cantnf 8550. 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 6643 . . . . . 6 (𝐺 supp ∅) ∈ V
2 cantnflem1.o . . . . . . 7 𝑂 = OrdIso( E , (𝐺 supp ∅))
32oion 8401 . . . . . 6 ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
41, 3mp1i 13 . . . . 5 (𝜑 → dom 𝑂 ∈ On)
5 uniexg 6920 . . . . 5 (dom 𝑂 ∈ On → dom 𝑂 ∈ V)
6 sucidg 5772 . . . . 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 8542 . . . . . . . . 9 (𝜑𝑋 ∈ (𝐺 supp ∅))
17 n0i 3902 . . . . . . . . 9 (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19 ovexd 6645 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) ∈ V)
208, 9, 10, 2, 13cantnfcl 8524 . . . . . . . . . . 11 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
2120simpld 475 . . . . . . . . . 10 (𝜑 → E We (𝐺 supp ∅))
222oien 8403 . . . . . . . . . 10 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
2319, 21, 22syl2anc 692 . . . . . . . . 9 (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24 breq1 4626 . . . . . . . . . 10 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25 ensymb 7964 . . . . . . . . . . 11 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26 en0 7979 . . . . . . . . . . 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 479 . . . . . . . 8 (𝜑 → dom 𝑂 ∈ ω)
32 nnlim 7040 . . . . . . . 8 (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
3331, 32syl 17 . . . . . . 7 (𝜑 → ¬ Lim dom 𝑂)
34 ioran 511 . . . . . . 7 (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
3530, 33, 34sylanbrc 697 . . . . . 6 (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
362oicl 8394 . . . . . . 7 Ord dom 𝑂
37 unizlim 5813 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3836, 37mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3935, 38mtbird 315 . . . . 5 (𝜑 → ¬ dom 𝑂 = dom 𝑂)
40 orduniorsuc 6992 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4136, 40mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4241ord 392 . . . . 5 (𝜑 → (¬ dom 𝑂 = dom 𝑂 → dom 𝑂 = suc dom 𝑂))
4339, 42mpd 15 . . . 4 (𝜑 → dom 𝑂 = suc dom 𝑂)
447, 43eleqtrrd 2701 . . 3 (𝜑 dom 𝑂 ∈ dom 𝑂)
452oiiso 8402 . . . . . . . 8 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
4619, 21, 45syl2anc 692 . . . . . . 7 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47 isof1o 6538 . . . . . . 7 (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
4846, 47syl 17 . . . . . 6 (𝜑𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
49 f1ocnv 6116 . . . . . 6 (𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) → 𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50 f1of 6104 . . . . . 6 (𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5148, 49, 503syl 18 . . . . 5 (𝜑𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5251, 16ffvelrnd 6326 . . . 4 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
53 elssuni 4440 . . . 4 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5452, 53syl 17 . . 3 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
5543, 31eqeltrrd 2699 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
56 peano2b 7043 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
5755, 56sylibr 224 . . . 4 (𝜑 dom 𝑂 ∈ ω)
58 eleq1 2686 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝑦 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
59 sseq2 3612 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ dom 𝑂))
6058, 59anbi12d 746 . . . . . . 7 (𝑦 = dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂)))
61 fveq2 6158 . . . . . . . . . . . 12 (𝑦 = dom 𝑂 → (𝑂𝑦) = (𝑂 dom 𝑂))
6261sseq2d 3618 . . . . . . . . . . 11 (𝑦 = dom 𝑂 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂 dom 𝑂)))
6362ifbid 4086 . . . . . . . . . 10 (𝑦 = dom 𝑂 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
6463mpteq2dv 4715 . . . . . . . . 9 (𝑦 = dom 𝑂 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
6564fveq2d 6162 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
66 suceq 5759 . . . . . . . . 9 (𝑦 = dom 𝑂 → suc 𝑦 = suc dom 𝑂)
6766fveq2d 6162 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc dom 𝑂))
6865, 67eleq12d 2692 . . . . . . 7 (𝑦 = dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
6960, 68imbi12d 334 . . . . . 6 (𝑦 = dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
7069imbi2d 330 . . . . 5 (𝑦 = dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))))
71 eleq1 2686 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72 sseq2 3612 . . . . . . . 8 (𝑦 = ∅ → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ ∅))
7371, 72anbi12d 746 . . . . . . 7 (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅)))
74 fveq2 6158 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑂𝑦) = (𝑂‘∅))
7574sseq2d 3618 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
7675ifbid 4086 . . . . . . . . . 10 (𝑦 = ∅ → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
7776mpteq2dv 4715 . . . . . . . . 9 (𝑦 = ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
7877fveq2d 6162 . . . . . . . 8 (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
79 suceq 5759 . . . . . . . . 9 (𝑦 = ∅ → suc 𝑦 = suc ∅)
8079fveq2d 6162 . . . . . . . 8 (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
8178, 80eleq12d 2692 . . . . . . 7 (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
8273, 81imbi12d 334 . . . . . 6 (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83 eleq1 2686 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂𝑢 ∈ dom 𝑂))
84 sseq2 3612 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ 𝑢))
8583, 84anbi12d 746 . . . . . . 7 (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)))
86 fveq2 6158 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑂𝑦) = (𝑂𝑢))
8786sseq2d 3618 . . . . . . . . . . 11 (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂𝑢)))
8887ifbid 4086 . . . . . . . . . 10 (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
8988mpteq2dv 4715 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
9089fveq2d 6162 . . . . . . . 8 (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))
91 suceq 5759 . . . . . . . . 9 (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
9291fveq2d 6162 . . . . . . . 8 (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
9390, 92eleq12d 2692 . . . . . . 7 (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
9485, 93imbi12d 334 . . . . . 6 (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95 eleq1 2686 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96 sseq2 3612 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ suc 𝑢))
9795, 96anbi12d 746 . . . . . . 7 (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢)))
98 fveq2 6158 . . . . . . . . . . . 12 (𝑦 = suc 𝑢 → (𝑂𝑦) = (𝑂‘suc 𝑢))
9998sseq2d 3618 . . . . . . . . . . 11 (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
10099ifbid 4086 . . . . . . . . . 10 (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
101100mpteq2dv 4715 . . . . . . . . 9 (𝑦 = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
102101fveq2d 6162 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
103 suceq 5759 . . . . . . . . 9 (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104103fveq2d 6162 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105102, 104eleq12d 2692 . . . . . . 7 (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
10697, 105imbi12d 334 . . . . . 6 (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107 f1ocnvfv2 6498 . . . . . . . . . . . . 13 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
10848, 16, 107syl2anc 692 . . . . . . . . . . . 12 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
109108sseq2d 3618 . . . . . . . . . . 11 (𝜑 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥𝑋))
110109ifbid 4086 . . . . . . . . . 10 (𝜑 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥𝑋, (𝐹𝑥), ∅))
111110mpteq2dv 4715 . . . . . . . . 9 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅)))
112111fveq2d 6162 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))))
113 cantnflem1.h . . . . . . . . 9 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐺‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 8545 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
115112, 114eqeltrd 2698 . . . . . . 7 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
116 ss0 3952 . . . . . . . . . . . . . 14 ((𝑂𝑋) ⊆ ∅ → (𝑂𝑋) = ∅)
117116fveq2d 6162 . . . . . . . . . . . . 13 ((𝑂𝑋) ⊆ ∅ → (𝑂‘(𝑂𝑋)) = (𝑂‘∅))
118117sseq2d 3618 . . . . . . . . . . . 12 ((𝑂𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119118ifbid 4086 . . . . . . . . . . 11 ((𝑂𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
120119mpteq2dv 4715 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
121120fveq2d 6162 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
122 suceq 5759 . . . . . . . . . . 11 ((𝑂𝑋) = ∅ → suc (𝑂𝑋) = suc ∅)
123116, 122syl 17 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → suc (𝑂𝑋) = suc ∅)
124123fveq2d 6162 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc ∅))
125121, 124eleq12d 2692 . . . . . . . 8 ((𝑂𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126125adantl 482 . . . . . . 7 ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127115, 126syl5ibcom 235 . . . . . 6 (𝜑 → ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128 ordelon 5716 . . . . . . . . . . . . 13 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
12936, 52, 128sylancr 694 . . . . . . . . . . . 12 (𝜑 → (𝑂𝑋) ∈ On)
130129adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
13136a1i 11 . . . . . . . . . . . 12 (𝜑 → Ord dom 𝑂)
132 ordelon 5716 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133131, 132sylan 488 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
134 onsseleq 5734 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
135130, 133, 134syl2anc 692 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
136 sucelon 6979 . . . . . . . . . . . . . . 15 (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
137133, 136sylibr 224 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
138 eloni 5702 . . . . . . . . . . . . . 14 (𝑢 ∈ On → Ord 𝑢)
139137, 138syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
140 ordsssuc 5781 . . . . . . . . . . . . 13 (((𝑂𝑋) ∈ On ∧ Ord 𝑢) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
141130, 139, 140syl2anc 692 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
142 ordtr 5706 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → Tr dom 𝑂)
14336, 142mp1i 13 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
144 simprl 793 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
145 trsuc 5779 . . . . . . . . . . . . . . . 16 ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
146143, 144, 145syl2anc 692 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
147 simprr 795 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ⊆ 𝑢)
148146, 147jca 554 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢))
1499adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
15010adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
151 oecl 7577 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝑜 𝐵) ∈ On)
152149, 150, 151syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 𝐵) ∈ On)
1538, 149, 150cantnff 8531 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴𝑜 𝐵))
1548, 9, 10cantnfs 8523 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
15512, 154mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
156155simpld 475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝐵𝐴)
157156ffvelrnda 6325 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → (𝐹𝑥) ∈ 𝐴)
1588, 9, 10cantnfs 8523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
15913, 158mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
160159simpld 475 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺:𝐵𝐴)
1618, 9, 10, 11, 12, 13, 14, 15oemapvali 8541 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑋𝐵 ∧ (𝐹𝑋) ∈ (𝐺𝑋) ∧ ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤))))
162161simp1d 1071 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
163160, 162ffvelrnd 6326 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐺𝑋) ∈ 𝐴)
164 ne0i 3903 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺𝑋) ∈ 𝐴𝐴 ≠ ∅)
165163, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ≠ ∅)
166 on0eln0 5749 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
1679, 166syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∅ ∈ 𝐴𝐴 ≠ ∅))
168165, 167mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∅ ∈ 𝐴)
169168adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → ∅ ∈ 𝐴)
170157, 169ifcld 4109 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ 𝐴)
171 eqid 2621 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
172170, 171fmptd 6351 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴)
173 mptexg 6449 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵 ∈ On → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
17410, 173syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
175 funmpt 5894 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
177155simprd 479 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 finSupp ∅)
178 eqid 2621 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹 supp ∅) = (𝐹 supp ∅)
179 eqimss2 3643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹 supp ∅) = (𝐹 supp ∅) → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
180178, 179mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
181 0ex 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ V
182181a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∅ ∈ V)
183156, 180, 10, 182suppssr 7286 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑥) = ∅)
184183ifeq1d 4082 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
185 ifid 4103 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑥 ⊆ (𝑂𝑢), ∅, ∅) = ∅
186184, 185syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
187186, 10suppss2 7289 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
188 fsuppsssupp 8251 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V ∧ Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
189174, 176, 177, 187, 188syl22anc 1324 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
1908, 9, 10cantnfs 8523 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴 ∧ (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)))
191172, 189, 190mpbir2and 956 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
192191adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
193153, 192ffvelrnd 6326 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵))
194 onelon 5717 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
195152, 193, 194syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
19631adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
197 elnn 7037 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
198144, 196, 197syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
199113cantnfvalf 8522 . . . . . . . . . . . . . . . . . . 19 𝐻:ω⟶On
200199ffvelrni 6324 . . . . . . . . . . . . . . . . . 18 (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
201198, 200syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
202 suppssdm 7268 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
203 fdm 6018 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
204160, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = 𝐵)
205202, 204syl5sseq 3638 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
206205adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
2072oif 8395 . . . . . . . . . . . . . . . . . . . . . . 23 𝑂:dom 𝑂⟶(𝐺 supp ∅)
208207ffvelrni 6324 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
209144, 208syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
210206, 209sseldd 3589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
211 onelon 5717 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
212150, 210, 211syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
213 oecl 7577 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
214149, 212, 213syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On)
215156adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐹:𝐵𝐴)
216215, 210ffvelrnd 6326 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
217 onelon 5717 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
218149, 216, 217syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
219 omcl 7576 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
220214, 218, 219syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
221 oaord 7587 . . . . . . . . . . . . . . . . 17 ((((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
222195, 201, 220, 221syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
223 ifeq1 4068 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
224 ifid 4103 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
225223, 224syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = ∅)
226 ifeq1 4068 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅))
227 ifid 4103 . . . . . . . . . . . . . . . . . . . . . . 23 if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅) = ∅
228226, 227syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = ∅)
229225, 228eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) ↔ ∅ = ∅))
230 onss 6952 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → 𝐵 ⊆ On)
23110, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ⊆ On)
232231sselda 3588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐵) → 𝑥 ∈ On)
233232adantlr 750 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → 𝑥 ∈ On)
234212adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑂‘suc 𝑢) ∈ On)
235 onsseleq 5734 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
236233, 234, 235syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
237236adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
238233adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → 𝑥 ∈ On)
239207ffvelrni 6324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ dom 𝑂 → (𝑂𝑢) ∈ (𝐺 supp ∅))
240146, 239syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝐺 supp ∅))
241206, 240sseldd 3589 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ 𝐵)
242 onelon 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ (𝑂𝑢) ∈ 𝐵) → (𝑂𝑢) ∈ On)
243150, 241, 242syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ On)
244243ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑂𝑢) ∈ On)
245 onsssuc 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
246238, 244, 245syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
247 vex 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑢 ∈ V
248247sucid 5773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ suc 𝑢
24946adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
250 isorel 6541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
251249, 146, 144, 250syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
252247sucex 6973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc 𝑢 ∈ V
253252epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 E suc 𝑢𝑢 ∈ suc 𝑢)
254 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑂‘suc 𝑢) ∈ V
255254epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
256251, 253, 2553bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢)))
257248, 256mpbii 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
258 eloni 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
259212, 258syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
260 ordelsuc 6982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑂𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
261243, 259, 260syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
262257, 261mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
263262ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
264263sseld 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
265246, 264sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
266 simprr 795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ 𝑥)
267249ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
270 f1ocnvfv2 6498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
271268, 269, 270syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂‘(𝑂𝑥)) = 𝑥)
272266, 271eleqtrrd 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
273146ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
274268, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
275274, 269ffvelrnd 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ dom 𝑂)
276 isorel 6541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
277267, 273, 275, 276syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
278 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂𝑥) ∈ V
279278epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 E (𝑂𝑥) ↔ 𝑢 ∈ (𝑂𝑥))
280 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂‘(𝑂𝑥)) ∈ V
281280epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑢) E (𝑂‘(𝑂𝑥)) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
282277, 279, 2813bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥))))
283272, 282mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ (𝑂𝑥))
284 ordelon 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂) → (𝑂𝑥) ∈ On)
28536, 275, 284sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ On)
286 eloni 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑥) ∈ On → Ord (𝑂𝑥))
287285, 286syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → Ord (𝑂𝑥))
288 ordelsuc 6982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢 ∈ (𝑂𝑥) ∧ Ord (𝑂𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
289283, 287, 288syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
290283, 289mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (𝑂𝑥))
291144ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
29236, 291, 132sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
293 ontri1 5726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc 𝑢 ∈ On ∧ (𝑂𝑥) ∈ On) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
294292, 285, 293syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
295290, 294mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ (𝑂𝑥) ∈ suc 𝑢)
296 isorel 6541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
297267, 275, 291, 296syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
298252epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑥) E suc 𝑢 ↔ (𝑂𝑥) ∈ suc 𝑢)
299254epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢))
300297, 298, 2993bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢)))
301271eleq1d 2683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
302300, 301bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢𝑥 ∈ (𝑂‘suc 𝑢)))
303295, 302mtbid 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
304303expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑂𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
305304con2d 129 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂𝑢) ∈ 𝑥))
306 ontri1 5726 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
307238, 244, 306syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
308305, 307sylibrd 249 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂𝑢)))
309265, 308impbid 202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
310309orbi1d 738 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
311237, 310bitr4d 271 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
312 orcom 402 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)))
313311, 312syl6bb 276 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢))))
314313ifbid 4086 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
315 eqidd 2622 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ∅ = ∅)
316229, 314, 315pm2.61ne 2875 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
317316mpteq2dva 4714 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)))
318317fveq2d 6162 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))))
319 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑥) ∈ V
320319, 181ifex 4134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V
321320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
322321ralrimivw 2963 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
323171fnmpt 5987 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
324322, 323syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
325181a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∅ ∈ V)
326 suppvalfn 7262 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅})
327 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝐵
328 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐵
329 nffvmpt1 6166 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)
330 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥
331329, 330nfne 2890 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅
332 nfv 1840 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅
333 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥))
334333neeq1d 2849 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅))
335327, 328, 331, 332, 334cbvrab 3188 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅}
336326, 335syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
337324, 150, 325, 336syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
338 eqidd 2622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
339320a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
340338, 339fvmpt2d 6260 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
341340neeq1d 2849 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
342339biantrurd 529 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)))
343 dif1o 7540 . . . . . . . . . . . . . . . . . . . . . . . . 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 3180 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
347337, 346eqtrd 2655 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)})
348320, 343mpbiran 952 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)
349 ifeq1 4068 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
350349, 185syl6eq 2671 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
351350necon3i 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → (𝐹𝑥) ≠ ∅)
352 iffalse 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ⊆ (𝑂𝑢) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
353352necon1ai 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂𝑢))
354351, 353jca 554 . . . . . . . . . . . . . . . . . . . . . . . . 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 1258 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵 ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
359358rabssdv 3667 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
360347, 359eqsstrd 3624 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
361 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
362 sseq1 3611 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑦 ⊆ (𝑂𝑢)))
363361, 362orbi12d 745 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢))))
364 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
365363, 364ifbieq1d 4087 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
366365cbvmptv 4720 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
367 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑂‘suc 𝑢) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
368367adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐵𝑦 = (𝑂‘suc 𝑢)) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
369368ifeq1da 4094 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
370362, 364ifbieq1d 4087 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
371 fvex 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑦) ∈ V
372371, 181ifex 4134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅) ∈ V
373370, 171, 372fvmpt 6249 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
374373ifeq2d 4083 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅)))
375 ifor 4113 . . . . . . . . . . . . . . . . . . . . . . . 24 if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
376374, 375syl6eqr 2673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
377369, 376eqtr3d 2657 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
378377mpteq2ia 4710 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦))) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
379366, 378eqtr4i 2646 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
3808, 149, 150, 192, 210, 216, 360, 379cantnfp1 8538 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))))
381380simprd 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
382318, 381eqtrd 2655 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
3838, 9, 10, 2, 13, 113cantnfsuc 8527 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
384198, 383syldan 487 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
385161simp3d 1073 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
386385adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
387108adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) = 𝑋)
388129adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ On)
389137adantrr 752 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
390 onsssuc 5782 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑂𝑋) ∈ On ∧ 𝑢 ∈ On) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
391388, 389, 390syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
392147, 391mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ suc 𝑢)
39352adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ dom 𝑂)
394 isorel 6541 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
395249, 393, 144, 394syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
396252epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂𝑋) E suc 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢)
397254epelc 4997 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
398395, 396, 3973bitr3g 302 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢)))
399392, 398mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
400387, 399eqeltrrd 2699 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
401 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → (𝑋𝑤𝑋 ∈ (𝑂‘suc 𝑢)))
402 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐹𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
403 fveq2 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐺𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
404402, 403eqeq12d 2636 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
405401, 404imbi12d 334 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑂‘suc 𝑢) → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
406405rspcv 3295 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
407210, 386, 400, 406syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
408407oveq2d 6631 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
409408oveq1d 6630 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
410384, 409eqtr4d 2658 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
411382, 410eleq12d 2692 . . . . . . . . . . . . . . . 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 6158 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑋) = suc 𝑢 → (𝑂‘(𝑂𝑋)) = (𝑂‘suc 𝑢))
418417sseq2d 3618 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
419418ifbid 4086 . . . . . . . . . . . . . . . . 17 ((𝑂𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
420419mpteq2dv 4715 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
421420fveq2d 6162 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
422 suceq 5759 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → suc (𝑂𝑋) = suc suc 𝑢)
423422fveq2d 6162 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc suc 𝑢))
424421, 423eleq12d 2692 . . . . . . . . . . . . . 14 ((𝑂𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
425115, 424syl5ibcom 235 . . . . . . . . . . . . 13 (𝜑 → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
426425adantr 481 . . . . . . . . . . . 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 395 . . . . . . . . . 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 7056 . . . . 5 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
43470, 433vtoclga 3262 . . . 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 714 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))
437156feqmptd 6216 . . . 4 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
438 eqeq2 2632 . . . . . 6 ((𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = (𝐹𝑥) ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
439 eqeq2 2632 . . . . . 6 (∅ = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = ∅ ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
440 eqidd 2622 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = (𝐹𝑥))
441207ffvelrni 6324 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
44244, 441syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
443205, 442sseldd 3589 . . . . . . . . . . . 12 (𝜑 → (𝑂 dom 𝑂) ∈ 𝐵)
444 onelon 5717 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑂 dom 𝑂) ∈ 𝐵) → (𝑂 dom 𝑂) ∈ On)
44510, 443, 444syl2anc 692 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) ∈ On)
446445adantr 481 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑂 dom 𝑂) ∈ On)
447 ontri1 5726 . . . . . . . . . 10 ((𝑥 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
448232, 446, 447syl2anc 692 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
449448con2bid 344 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)))
450 simprl 793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥𝐵)
451385adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
452 eloni 5702 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) ∈ On → Ord (𝑂𝑋))
453129, 452syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord (𝑂𝑋))
454 orduni 6956 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑂 → Ord dom 𝑂)
45536, 454ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord dom 𝑂
456 ordtri1 5725 . . . . . . . . . . . . . . . . 17 ((Ord (𝑂𝑋) ∧ Ord dom 𝑂) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
457453, 455, 456sylancl 693 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
45854, 457mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
459 isorel 6541 . . . . . . . . . . . . . . . . . 18 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
46046, 44, 52, 459syl12anc 1321 . . . . . . . . . . . . . . . . 17 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
461 fvex 6168 . . . . . . . . . . . . . . . . . 18 (𝑂𝑋) ∈ V
462461epelc 4997 . . . . . . . . . . . . . . . . 17 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
463 fvex 6168 . . . . . . . . . . . . . . . . . 18 (𝑂‘(𝑂𝑋)) ∈ V
464463epelc 4997 . . . . . . . . . . . . . . . . 17 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
465460, 462, 4643bitr3g 302 . . . . . . . . . . . . . . . 16 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
466108eleq2d 2684 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
467465, 466bitrd 268 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
468458, 467mtbid 314 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
469 onelon 5717 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
47010, 162, 469syl2anc 692 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ On)
471 ontri1 5726 . . . . . . . . . . . . . . 15 ((𝑋 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
472470, 445, 471syl2anc 692 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
473468, 472mpbird 247 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (𝑂 dom 𝑂))
474473adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂 dom 𝑂))
475 simprr 795 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝑂 dom 𝑂) ∈ 𝑥)
476470adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
477232adantrr 752 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
478 ontr2 5741 . . . . . . . . . . . . 13 ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
479476, 477, 478syl2anc 692 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
480474, 475, 479mp2and 714 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋𝑥)
481 eleq2 2687 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑋𝑤𝑋𝑥))
482 fveq2 6158 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
483 fveq2 6158 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐺𝑤) = (𝐺𝑥))
484482, 483eqeq12d 2636 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹𝑥) = (𝐺𝑥)))
485481, 484imbi12d 334 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
486485rspcv 3295 . . . . . . . . . . 11 (𝑥𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
487450, 451, 480, 486syl3c 66 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = (𝐺𝑥))
488475adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂 dom 𝑂) ∈ 𝑥)
48946ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
49044ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ dom 𝑂)
49151ad2antrr 761 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
492 ffvelrn 6323 . . . . . . . . . . . . . . . . . 18 ((𝑂:(𝐺 supp ∅)⟶dom 𝑂𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
493491, 492sylancom 700 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
494 isorel 6541 . . . . . . . . . . . . . . . . 17 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
495489, 490, 493, 494syl12anc 1321 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
496278epelc 4997 . . . . . . . . . . . . . . . 16 ( dom 𝑂 E (𝑂𝑥) ↔ dom 𝑂 ∈ (𝑂𝑥))
497280epelc 4997 . . . . . . . . . . . . . . . 16 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)))
498495, 496, 4973bitr3g 302 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥))))
49948ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
500499, 270sylancom 700 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
501500eleq2d 2684 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
502498, 501bitrd 268 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
503488, 502mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ (𝑂𝑥))
504 elssuni 4440 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∈ dom 𝑂 → (𝑂𝑥) ⊆ dom 𝑂)
505493, 504syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ⊆ dom 𝑂)
50636, 493, 284sylancr 694 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ On)
507506, 286syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (𝑂𝑥))
508 ordtri1 5725 . . . . . . . . . . . . . . 15 ((Ord (𝑂𝑥) ∧ Ord dom 𝑂) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
509507, 455, 508sylancl 693 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
510505, 509mpbid 222 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ dom 𝑂 ∈ (𝑂𝑥))
511503, 510pm2.65da 599 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
512450, 511eldifd 3571 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
513 ssid 3609 . . . . . . . . . . . . 13 (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
514513a1i 11 . . . . . . . . . . . 12 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
515160, 514, 10, 182suppssr 7286 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑥) = ∅)
516512, 515syldan 487 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐺𝑥) = ∅)
517487, 516eqtrd 2655 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = ∅)
518517expr 642 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 → (𝐹𝑥) = ∅))
519449, 518sylbird 250 . . . . . . 7 ((𝜑𝑥𝐵) → (¬ 𝑥 ⊆ (𝑂 dom 𝑂) → (𝐹𝑥) = ∅))
520519imp 445 . . . . . 6 (((𝜑𝑥𝐵) ∧ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = ∅)
521438, 439, 440, 520ifbothda 4101 . . . . 5 ((𝜑𝑥𝐵) → (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
522521mpteq2dva 4714 . . . 4 (𝜑 → (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
523437, 522eqtrd 2655 . . 3 (𝜑𝐹 = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
524523fveq2d 6162 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
5258, 9, 10, 2, 13, 113cantnfval 8525 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
52643fveq2d 6162 . . 3 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
527525, 526eqtrd 2655 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc dom 𝑂))
528436, 524, 5273eltr4d 2713 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  {crab 2912  Vcvv 3190  cdif 3557  wss 3560  c0 3897  ifcif 4064   cuni 4409   class class class wbr 4623  {copab 4682  cmpt 4683  Tr wtr 4722   E cep 4993   We wwe 5042  ccnv 5083  dom cdm 5084  Ord word 5691  Oncon0 5692  Lim wlim 5693  suc csuc 5694  Fun wfun 5851   Fn wfn 5852  wf 5853  1-1-ontowf1o 5856  cfv 5857   Isom wiso 5858  (class class class)co 6615  cmpt2 6617  ωcom 7027   supp csupp 7255  seq𝜔cseqom 7502  1𝑜c1o 7513   +𝑜 coa 7517   ·𝑜 comu 7518  𝑜 coe 7519  cen 7912   finSupp cfsupp 8235  OrdIsocoi 8374   CNF ccnf 8518
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-supp 7256  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-seqom 7503  df-1o 7520  df-2o 7521  df-oadd 7524  df-omul 7525  df-oexp 7526  df-er 7702  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fsupp 8236  df-oi 8375  df-cnf 8519
This theorem is referenced by:  cantnf  8550
  Copyright terms: Public domain W3C validator