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

Theorem cantnflem1 9144
 Description: Lemma for cantnf 9148. 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 ↦ (((𝐴o (𝑂𝑘)) ·o (𝐺‘(𝑂𝑘))) +o 𝑧)), ∅)
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 7184 . . . . . 6 (𝐺 supp ∅) ∈ V
2 cantnflem1.o . . . . . . 7 𝑂 = OrdIso( E , (𝐺 supp ∅))
32oion 8992 . . . . . 6 ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
41, 3mp1i 13 . . . . 5 (𝜑 → dom 𝑂 ∈ On)
5 uniexg 7460 . . . . 5 (dom 𝑂 ∈ On → dom 𝑂 ∈ V)
6 sucidg 6266 . . . . 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 9140 . . . . . . . . 9 (𝜑𝑋 ∈ (𝐺 supp ∅))
17 n0i 4302 . . . . . . . . 9 (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19 ovexd 7186 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) ∈ V)
208, 9, 10, 2, 13cantnfcl 9122 . . . . . . . . . . 11 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
2120simpld 495 . . . . . . . . . 10 (𝜑 → E We (𝐺 supp ∅))
222oien 8994 . . . . . . . . . 10 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
2319, 21, 22syl2anc 584 . . . . . . . . 9 (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24 breq1 5065 . . . . . . . . . 10 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25 ensymb 8549 . . . . . . . . . . 11 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26 en0 8564 . . . . . . . . . . 11 ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
2725, 26bitri 276 . . . . . . . . . 10 (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
2824, 27syl6bb 288 . . . . . . . . 9 (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
2923, 28syl5ibcom 246 . . . . . . . 8 (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
3018, 29mtod 199 . . . . . . 7 (𝜑 → ¬ dom 𝑂 = ∅)
3120simprd 496 . . . . . . . 8 (𝜑 → dom 𝑂 ∈ ω)
32 nnlim 7584 . . . . . . . 8 (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
3331, 32syl 17 . . . . . . 7 (𝜑 → ¬ Lim dom 𝑂)
34 ioran 979 . . . . . . 7 (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
3530, 33, 34sylanbrc 583 . . . . . 6 (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
362oicl 8985 . . . . . . 7 Ord dom 𝑂
37 unizlim 6304 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3836, 37mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
3935, 38mtbird 326 . . . . 5 (𝜑 → ¬ dom 𝑂 = dom 𝑂)
40 orduniorsuc 7536 . . . . . . 7 (Ord dom 𝑂 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4136, 40mp1i 13 . . . . . 6 (𝜑 → (dom 𝑂 = dom 𝑂 ∨ dom 𝑂 = suc dom 𝑂))
4241ord 860 . . . . 5 (𝜑 → (¬ dom 𝑂 = dom 𝑂 → dom 𝑂 = suc dom 𝑂))
4339, 42mpd 15 . . . 4 (𝜑 → dom 𝑂 = suc dom 𝑂)
447, 43eleqtrrd 2920 . . 3 (𝜑 dom 𝑂 ∈ dom 𝑂)
452oiiso 8993 . . . . . . . 8 (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
4619, 21, 45syl2anc 584 . . . . . . 7 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47 isof1o 7071 . . . . . . 7 (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
4846, 47syl 17 . . . . . 6 (𝜑𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
49 f1ocnv 6623 . . . . . 6 (𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) → 𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50 f1of 6611 . . . . . 6 (𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5148, 49, 503syl 18 . . . . 5 (𝜑𝑂:(𝐺 supp ∅)⟶dom 𝑂)
5251, 16ffvelrnd 6847 . . . 4 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
53 elssuni 4865 . . . 4 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5452, 53syl 17 . . 3 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
5543, 31eqeltrrd 2918 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
56 peano2b 7587 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
5755, 56sylibr 235 . . . 4 (𝜑 dom 𝑂 ∈ ω)
58 eleq1 2904 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝑦 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
59 sseq2 3996 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ dom 𝑂))
6058, 59anbi12d 630 . . . . . . 7 (𝑦 = dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂)))
61 fveq2 6666 . . . . . . . . . . . 12 (𝑦 = dom 𝑂 → (𝑂𝑦) = (𝑂 dom 𝑂))
6261sseq2d 4002 . . . . . . . . . . 11 (𝑦 = dom 𝑂 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂 dom 𝑂)))
6362ifbid 4491 . . . . . . . . . 10 (𝑦 = dom 𝑂 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
6463mpteq2dv 5158 . . . . . . . . 9 (𝑦 = dom 𝑂 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
6564fveq2d 6670 . . . . . . . 8 (𝑦 = dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
66 suceq 6253 . . . . . . . . 9 (𝑦 = dom 𝑂 → suc 𝑦 = suc dom 𝑂)
6766fveq2d 6670 . . . . . . . 8 (𝑦 = dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc dom 𝑂))
6865, 67eleq12d 2911 . . . . . . 7 (𝑦 = dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
6960, 68imbi12d 346 . . . . . 6 (𝑦 = dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
7069imbi2d 342 . . . . 5 (𝑦 = dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))))
71 eleq1 2904 . . . . . . . 8 (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72 sseq2 3996 . . . . . . . 8 (𝑦 = ∅ → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ ∅))
7371, 72anbi12d 630 . . . . . . 7 (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅)))
74 fveq2 6666 . . . . . . . . . . . 12 (𝑦 = ∅ → (𝑂𝑦) = (𝑂‘∅))
7574sseq2d 4002 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
7675ifbid 4491 . . . . . . . . . 10 (𝑦 = ∅ → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
7776mpteq2dv 5158 . . . . . . . . 9 (𝑦 = ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
7877fveq2d 6670 . . . . . . . 8 (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
79 suceq 6253 . . . . . . . . 9 (𝑦 = ∅ → suc 𝑦 = suc ∅)
8079fveq2d 6670 . . . . . . . 8 (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
8178, 80eleq12d 2911 . . . . . . 7 (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
8273, 81imbi12d 346 . . . . . 6 (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83 eleq1 2904 . . . . . . . 8 (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂𝑢 ∈ dom 𝑂))
84 sseq2 3996 . . . . . . . 8 (𝑦 = 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ 𝑢))
8583, 84anbi12d 630 . . . . . . 7 (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)))
86 fveq2 6666 . . . . . . . . . . . 12 (𝑦 = 𝑢 → (𝑂𝑦) = (𝑂𝑢))
8786sseq2d 4002 . . . . . . . . . . 11 (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂𝑢)))
8887ifbid 4491 . . . . . . . . . 10 (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
8988mpteq2dv 5158 . . . . . . . . 9 (𝑦 = 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
9089fveq2d 6670 . . . . . . . 8 (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))
91 suceq 6253 . . . . . . . . 9 (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
9291fveq2d 6670 . . . . . . . 8 (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
9390, 92eleq12d 2911 . . . . . . 7 (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
9485, 93imbi12d 346 . . . . . 6 (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95 eleq1 2904 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96 sseq2 3996 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝑂𝑋) ⊆ 𝑦 ↔ (𝑂𝑋) ⊆ suc 𝑢))
9795, 96anbi12d 630 . . . . . . 7 (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢)))
98 fveq2 6666 . . . . . . . . . . . 12 (𝑦 = suc 𝑢 → (𝑂𝑦) = (𝑂‘suc 𝑢))
9998sseq2d 4002 . . . . . . . . . . 11 (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
10099ifbid 4491 . . . . . . . . . 10 (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
101100mpteq2dv 5158 . . . . . . . . 9 (𝑦 = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
102101fveq2d 6670 . . . . . . . 8 (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
103 suceq 6253 . . . . . . . . 9 (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104103fveq2d 6670 . . . . . . . 8 (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105102, 104eleq12d 2911 . . . . . . 7 (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
10697, 105imbi12d 346 . . . . . 6 (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107 f1ocnvfv2 7031 . . . . . . . . . . . . 13 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
10848, 16, 107syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
109108sseq2d 4002 . . . . . . . . . . 11 (𝜑 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥𝑋))
110109ifbid 4491 . . . . . . . . . 10 (𝜑 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥𝑋, (𝐹𝑥), ∅))
111110mpteq2dv 5158 . . . . . . . . 9 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅)))
112111fveq2d 6670 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))))
113 cantnflem1.h . . . . . . . . 9 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝑂𝑘)) ·o (𝐺‘(𝑂𝑘))) +o 𝑧)), ∅)
1148, 9, 10, 11, 12, 13, 14, 15, 2, 113cantnflem1d 9143 . . . . . . . 8 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥𝑋, (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
115112, 114eqeltrd 2917 . . . . . . 7 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)))
116 ss0 4355 . . . . . . . . . . . . . 14 ((𝑂𝑋) ⊆ ∅ → (𝑂𝑋) = ∅)
117116fveq2d 6670 . . . . . . . . . . . . 13 ((𝑂𝑋) ⊆ ∅ → (𝑂‘(𝑂𝑋)) = (𝑂‘∅))
118117sseq2d 4002 . . . . . . . . . . . 12 ((𝑂𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119118ifbid 4491 . . . . . . . . . . 11 ((𝑂𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))
120119mpteq2dv 5158 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅)))
121120fveq2d 6670 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))))
122 suceq 6253 . . . . . . . . . . 11 ((𝑂𝑋) = ∅ → suc (𝑂𝑋) = suc ∅)
123116, 122syl 17 . . . . . . . . . 10 ((𝑂𝑋) ⊆ ∅ → suc (𝑂𝑋) = suc ∅)
124123fveq2d 6670 . . . . . . . . 9 ((𝑂𝑋) ⊆ ∅ → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc ∅))
125121, 124eleq12d 2911 . . . . . . . 8 ((𝑂𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126125adantl 482 . . . . . . 7 ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127115, 126syl5ibcom 246 . . . . . 6 (𝜑 → ((∅ ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128 ordelon 6212 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
12936, 52, 128sylancr 587 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
13036a1i 11 . . . . . . . . . . . 12 (𝜑 → Ord dom 𝑂)
131 ordelon 6212 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
132130, 131sylan 580 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133 onsseleq 6229 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
134129, 132, 133syl2an2r 681 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 ↔ ((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢)))
135 sucelon 7523 . . . . . . . . . . . . . . 15 (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
136132, 135sylibr 235 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
137 eloni 6198 . . . . . . . . . . . . . 14 (𝑢 ∈ On → Ord 𝑢)
138136, 137syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
139 ordsssuc 6274 . . . . . . . . . . . . 13 (((𝑂𝑋) ∈ On ∧ Ord 𝑢) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
140129, 138, 139syl2an2r 681 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
141 ordtr 6202 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → Tr dom 𝑂)
14236, 141mp1i 13 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
143 simprl 767 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
144 trsuc 6272 . . . . . . . . . . . . . . . 16 ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
145142, 143, 144syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
146 simprr 769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ⊆ 𝑢)
147145, 146jca 512 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢))
14810adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
149 oecl 8156 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴o 𝐵) ∈ On)
1509, 148, 149syl2an2r 681 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴o 𝐵) ∈ On)
1519adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
1528, 151, 148cantnff 9129 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴o 𝐵))
1538, 9, 10cantnfs 9121 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹𝑆 ↔ (𝐹:𝐵𝐴𝐹 finSupp ∅)))
15412, 153mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (𝐹:𝐵𝐴𝐹 finSupp ∅))
155154simpld 495 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐹:𝐵𝐴)
156155ffvelrnda 6846 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → (𝐹𝑥) ∈ 𝐴)
1578, 9, 10cantnfs 9121 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
15813, 157mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
159158simpld 495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝐺:𝐵𝐴)
1608, 9, 10, 11, 12, 13, 14, 15oemapvali 9139 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑋𝐵 ∧ (𝐹𝑋) ∈ (𝐺𝑋) ∧ ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤))))
161160simp1d 1136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝜑𝑋𝐵)
162159, 161ffvelrnd 6847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐺𝑋) ∈ 𝐴)
163162ne0d 4304 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ≠ ∅)
164 on0eln0 6243 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ On → (∅ ∈ 𝐴𝐴 ≠ ∅))
1659, 164syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → (∅ ∈ 𝐴𝐴 ≠ ∅))
166163, 165mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ∅ ∈ 𝐴)
167166adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥𝐵) → ∅ ∈ 𝐴)
168156, 167ifcld 4514 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ 𝐴)
169168fmpttd 6874 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴)
17010mptexd 6985 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V)
171 funmpt 6389 . . . . . . . . . . . . . . . . . . . . . . 23 Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
173154simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹 finSupp ∅)
174 ssidd 3993 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
175 0ex 5207 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ∅ ∈ V
176175a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝜑 → ∅ ∈ V)
177155, 174, 10, 176suppssr 7855 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑥) = ∅)
178177ifeq1d 4487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
179 ifid 4508 . . . . . . . . . . . . . . . . . . . . . . . 24 if(𝑥 ⊆ (𝑂𝑢), ∅, ∅) = ∅
180178, 179syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
181180, 10suppss2 7858 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
182 fsuppsssupp 8841 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ V ∧ Fun (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
183170, 172, 173, 181, 182syl22anc 836 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)
1848, 9, 10cantnfs 9121 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)):𝐵𝐴 ∧ (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) finSupp ∅)))
185169, 183, 184mpbir2and 709 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
186185adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) ∈ 𝑆)
187152, 186ffvelrnd 6847 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴o 𝐵))
188 onelon 6213 . . . . . . . . . . . . . . . . . 18 (((𝐴o 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐴o 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
189150, 187, 188syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On)
19031adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
191 elnn 7581 . . . . . . . . . . . . . . . . . . 19 ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
192143, 190, 191syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
193113cantnfvalf 9120 . . . . . . . . . . . . . . . . . . 19 𝐻:ω⟶On
194193ffvelrni 6845 . . . . . . . . . . . . . . . . . 18 (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
195192, 194syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
196 suppssdm 7837 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
197196, 159fssdm 6526 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
198197adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
1992oif 8986 . . . . . . . . . . . . . . . . . . . . . . 23 𝑂:dom 𝑂⟶(𝐺 supp ∅)
200199ffvelrni 6845 . . . . . . . . . . . . . . . . . . . . . 22 (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
201143, 200syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
202198, 201sseldd 3971 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
203 onelon 6213 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
20410, 202, 203syl2an2r 681 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
205 oecl 8156 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴o (𝑂‘suc 𝑢)) ∈ On)
2069, 204, 205syl2an2r 681 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐴o (𝑂‘suc 𝑢)) ∈ On)
207155adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝐹:𝐵𝐴)
208207, 202ffvelrnd 6847 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
209 onelon 6213 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
2109, 208, 209syl2an2r 681 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
211 omcl 8155 . . . . . . . . . . . . . . . . . 18 (((𝐴o (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
212206, 210, 211syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
213 oaord 8166 . . . . . . . . . . . . . . . . 17 ((((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
214189, 195, 212, 213syl3anc 1365 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
215 ifeq1 4473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
216 ifid 4508 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
217215, 216syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = ∅)
218 ifeq1 4473 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅))
219 ifid 4508 . . . . . . . . . . . . . . . . . . . . . . 23 if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), ∅, ∅) = ∅
220218, 219syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = ∅)
221217, 220eqeq12d 2841 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) ↔ ∅ = ∅))
222 onss 7496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐵 ∈ On → 𝐵 ⊆ On)
22310, 222syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑𝐵 ⊆ On)
224223sselda 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑥𝐵) → 𝑥 ∈ On)
225224adantlr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → 𝑥 ∈ On)
226204adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑂‘suc 𝑢) ∈ On)
227 onsseleq 6229 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
228225, 226, 227syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
229228adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
230199ffvelrni 6845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 ∈ dom 𝑂 → (𝑂𝑢) ∈ (𝐺 supp ∅))
231145, 230syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝐺 supp ∅))
232198, 231sseldd 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ 𝐵)
233 onelon 6213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐵 ∈ On ∧ (𝑂𝑢) ∈ 𝐵) → (𝑂𝑢) ∈ On)
23410, 232, 233syl2an2r 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ On)
235234ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑂𝑢) ∈ On)
236 onsssuc 6275 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
237225, 235, 236syl2an2r 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ suc (𝑂𝑢)))
238 vex 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑢 ∈ V
239238sucid 6267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑢 ∈ suc 𝑢
24046adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
241 isorel 7074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
242240, 145, 143, 241syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂𝑢) E (𝑂‘suc 𝑢)))
243238sucex 7517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 suc 𝑢 ∈ V
244243epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑢 E suc 𝑢𝑢 ∈ suc 𝑢)
245 fvex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑂‘suc 𝑢) ∈ V
246245epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
247242, 244, 2463bitr3g 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂𝑢) ∈ (𝑂‘suc 𝑢)))
248239, 247mpbii 234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑢) ∈ (𝑂‘suc 𝑢))
249 eloni 6198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
250204, 249syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
251 ordelsuc 7526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝑂𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
252234, 250, 251syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢)))
253248, 252mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
254253ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → suc (𝑂𝑢) ⊆ (𝑂‘suc 𝑢))
255254sseld 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
256237, 255sylbid 241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
257 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ 𝑥)
258240ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
259258, 47syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
2608, 9, 10, 11, 12, 13, 14, 15, 2cantnflem1c 9142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
261 f1ocnvfv2 7031 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
262259, 260, 261syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂‘(𝑂𝑥)) = 𝑥)
263257, 262eleqtrrd 2920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
264145ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
265259, 49, 503syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
266265, 260ffvelrnd 6847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ dom 𝑂)
267 isorel 7074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
268258, 264, 266, 267syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 E (𝑂𝑥) ↔ (𝑂𝑢) E (𝑂‘(𝑂𝑥))))
269 fvex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂𝑥) ∈ V
270269epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑢 E (𝑂𝑥) ↔ 𝑢 ∈ (𝑂𝑥))
271 fvex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑂‘(𝑂𝑥)) ∈ V
272271epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑢) E (𝑂‘(𝑂𝑥)) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥)))
273268, 270, 2723bitr3g 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ (𝑂𝑢) ∈ (𝑂‘(𝑂𝑥))))
274263, 273mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → 𝑢 ∈ (𝑂𝑥))
275 ordelon 6212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((Ord dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂) → (𝑂𝑥) ∈ On)
27636, 266, 275sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑂𝑥) ∈ On)
277 eloni 6198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑂𝑥) ∈ On → Ord (𝑂𝑥))
278276, 277syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → Ord (𝑂𝑥))
279 ordelsuc 7526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑢 ∈ (𝑂𝑥) ∧ Ord (𝑂𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
280274, 278, 279syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (𝑢 ∈ (𝑂𝑥) ↔ suc 𝑢 ⊆ (𝑂𝑥)))
281274, 280mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (𝑂𝑥))
282143ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
28336, 282, 131sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
284 ontri1 6222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((suc 𝑢 ∈ On ∧ (𝑂𝑥) ∈ On) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
285283, 276, 284syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (𝑂𝑥) ↔ ¬ (𝑂𝑥) ∈ suc 𝑢))
286281, 285mpbid 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ (𝑂𝑥) ∈ suc 𝑢)
287 isorel 7074 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
288258, 266, 282, 287syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) E suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢)))
289243epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂𝑥) E suc 𝑢 ↔ (𝑂𝑥) ∈ suc 𝑢)
290245epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑂‘(𝑂𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢))
291288, 289, 2903bitr3g 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢)))
292262eleq1d 2901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂‘(𝑂𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
293291, 292bitrd 280 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ((𝑂𝑥) ∈ suc 𝑢𝑥 ∈ (𝑂‘suc 𝑢)))
294286, 293mtbid 325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ ((𝐹𝑥) ≠ ∅ ∧ (𝑂𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
295294expr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑂𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
296295con2d 136 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂𝑢) ∈ 𝑥))
297 ontri1 6222 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑥 ∈ On ∧ (𝑂𝑢) ∈ On) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
298225, 235, 297syl2an2r 681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ ¬ (𝑂𝑢) ∈ 𝑥))
299296, 298sylibrd 260 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂𝑢)))
300256, 299impbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
301300orbi1d 912 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
302229, 301bitr4d 283 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
303 orcom 866 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ⊆ (𝑂𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)))
304302, 303syl6bb 288 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢))))
305304ifbid 4491 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) ∧ (𝐹𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
306 eqidd 2826 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ∅ = ∅)
307221, 305, 306pm2.61ne 3106 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))
308307mpteq2dva 5157 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)))
309308fveq2d 6670 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))))
310 fvex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑥) ∈ V
311310, 175ifex 4517 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V
312311a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
313312ralrimivw 3187 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
314 eqid 2825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
315314fnmpt 6484 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑥𝐵 if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
316313, 315syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵)
317175a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∅ ∈ V)
318 suppvalfn 7831 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅})
319 nfcv 2981 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦𝐵
320 nfcv 2981 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥𝐵
321 nffvmpt1 6677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)
322 nfcv 2981 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑥
323321, 322nfne 3123 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑥((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅
324 nfv 1908 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅
325 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦 = 𝑥 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥))
326325neeq1d 3079 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑥 → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅))
327319, 320, 323, 324, 326cbvrabw 3494 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑦𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅}
328318, 327syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
329316, 148, 317, 328syl3anc 1365 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅})
330 eqidd 2826 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))
331311a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V)
332330, 331fvmpt2d 6776 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))
333332neeq1d 3079 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
334331biantrurd 533 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)))
335 dif1o 8119 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o) ↔ (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅))
336334, 335syl6bbr 290 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)))
337333, 336bitrd 280 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)))
338337rabbidva 3483 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)})
339329, 338eqtrd 2860 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) = {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)})
340311, 335mpbiran 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o) ↔ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅)
341 ifeq1 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂𝑢), ∅, ∅))
342341, 179syl6eq 2876 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹𝑥) = ∅ → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
343342necon3i 3052 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → (𝐹𝑥) ≠ ∅)
344 iffalse 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑥 ⊆ (𝑂𝑢) → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = ∅)
345344necon1ai 3047 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂𝑢))
346343, 345jca 512 . . . . . . . . . . . . . . . . . . . . . . . . 25 (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → ((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)))
347256expimpd 454 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (((𝐹𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
348346, 347syl5 34 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
349340, 348syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵) → (if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o) → 𝑥 ∈ (𝑂‘suc 𝑢)))
3503493impia 1111 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) ∧ 𝑥𝐵 ∧ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)) → 𝑥 ∈ (𝑂‘suc 𝑢))
351350rabssdv 4054 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → {𝑥𝐵 ∣ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) ∈ (V ∖ 1o)} ⊆ (𝑂‘suc 𝑢))
352339, 351eqsstrd 4008 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
353 eqeq1 2829 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
354 sseq1 3995 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂𝑢) ↔ 𝑦 ⊆ (𝑂𝑢)))
355353, 354orbi12d 914 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢))))
356 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
357355, 356ifbieq1d 4492 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
358357cbvmptv 5165 . . . . . . . . . . . . . . . . . . . . 21 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
359 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = (𝑂‘suc 𝑢) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
360359adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐵𝑦 = (𝑂‘suc 𝑢)) → (𝐹𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
361360ifeq1da 4499 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
362354, 356ifbieq1d 4492 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
363 fvex 6679 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐹𝑦) ∈ V
364363, 175ifex 4517 . . . . . . . . . . . . . . . . . . . . . . . . . 26 if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅) ∈ V
365362, 314, 364fvmpt 6764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦𝐵 → ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
366365ifeq2d 4488 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅)))
367 ifor 4521 . . . . . . . . . . . . . . . . . . . . . . . 24 if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), if(𝑦 ⊆ (𝑂𝑢), (𝐹𝑦), ∅))
368366, 367syl6eqr 2878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹𝑦), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
369361, 368eqtr3d 2862 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
370369mpteq2ia 5153 . . . . . . . . . . . . . . . . . . . . 21 (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦))) = (𝑦𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂𝑢)), (𝐹𝑦), ∅))
371358, 370eqtr4i 2851 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) = (𝑦𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))‘𝑦)))
3728, 151, 148, 186, 202, 208, 352, 371cantnfp1 9136 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))))))
373372simprd 496 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂𝑢)), (𝐹𝑥), ∅))) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
374309, 373eqtrd 2860 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))))
3758, 9, 10, 2, 13, 113cantnfsuc 9125 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
376192, 375syldan 591 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
377160simp3d 1138 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
378377adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
379108adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) = 𝑋)
380136adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
381 onsssuc 6275 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑂𝑋) ∈ On ∧ 𝑢 ∈ On) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
382129, 380, 381syl2an2r 681 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ⊆ 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢))
383146, 382mpbid 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ suc 𝑢)
38452adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂𝑋) ∈ dom 𝑂)
385 isorel 7074 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((𝑂𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
386240, 384, 143, 385syl12anc 834 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) E suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢)))
387243epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂𝑋) E suc 𝑢 ↔ (𝑂𝑋) ∈ suc 𝑢)
388245epeli 5466 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂‘(𝑂𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
389386, 387, 3883bitr3g 314 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝑂𝑋) ∈ suc 𝑢 ↔ (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢)))
390383, 389mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝑂‘(𝑂𝑋)) ∈ (𝑂‘suc 𝑢))
391379, 390eqeltrrd 2918 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
392 eleq2 2905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → (𝑋𝑤𝑋 ∈ (𝑂‘suc 𝑢)))
393 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐹𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
394 fveq2 6666 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 = (𝑂‘suc 𝑢) → (𝐺𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
395393, 394eqeq12d 2841 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = (𝑂‘suc 𝑢) → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
396392, 395imbi12d 346 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = (𝑂‘suc 𝑢) → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
397396rspcv 3621 . . . . . . . . . . . . . . . . . . . . 21 ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
398202, 378, 391, 397syl3c 66 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
399398oveq2d 7167 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → ((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))))
400399oveq1d 7166 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
401376, 400eqtr4d 2863 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
402374, 401eleq12d 2911 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅)))) ∈ (((𝐴o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
403214, 402bitr4d 283 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
404403biimpd 230 . . . . . . . . . . . . . 14 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
405147, 404embantd 59 . . . . . . . . . . . . 13 ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
406405expr 457 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
407140, 406sylbird 261 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
408 fveq2 6666 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑋) = suc 𝑢 → (𝑂‘(𝑂𝑋)) = (𝑂‘suc 𝑢))
409408sseq2d 4002 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(𝑂𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
410409ifbid 4491 . . . . . . . . . . . . . . . . 17 ((𝑂𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))
411410mpteq2dv 5158 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅)))
412411fveq2d 6670 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))))
413 suceq 6253 . . . . . . . . . . . . . . . 16 ((𝑂𝑋) = suc 𝑢 → suc (𝑂𝑋) = suc suc 𝑢)
414413fveq2d 6670 . . . . . . . . . . . . . . 15 ((𝑂𝑋) = suc 𝑢 → (𝐻‘suc (𝑂𝑋)) = (𝐻‘suc suc 𝑢))
415412, 414eleq12d 2911 . . . . . . . . . . . . . 14 ((𝑂𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘(𝑂𝑋)), (𝐹𝑥), ∅))) ∈ (𝐻‘suc (𝑂𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
416115, 415syl5ibcom 246 . . . . . . . . . . . . 13 (𝜑 → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
417416adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
418417a1dd 50 . . . . . . . . . . 11 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
419407, 418jaod 855 . . . . . . . . . 10 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((𝑂𝑋) ∈ suc 𝑢 ∨ (𝑂𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
420134, 419sylbid 241 . . . . . . . . 9 ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((𝑂𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
421420expimpd 454 . . . . . . . 8 (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
422421com23 86 . . . . . . 7 (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
423422a1i 11 . . . . . 6 (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
42482, 94, 106, 127, 423finds2 7601 . . . . 5 (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂𝑦), (𝐹𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
42570, 424vtoclga 3578 . . . 4 ( dom 𝑂 ∈ ω → (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))))
42657, 425mpcom 38 . . 3 (𝜑 → (( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ⊆ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂)))
42744, 54, 426mp2and 695 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))) ∈ (𝐻‘suc dom 𝑂))
428155feqmptd 6729 . . . 4 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
429 eqeq2 2837 . . . . . 6 ((𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = (𝐹𝑥) ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
430 eqeq2 2837 . . . . . 6 (∅ = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅) → ((𝐹𝑥) = ∅ ↔ (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
431 eqidd 2826 . . . . . 6 (((𝜑𝑥𝐵) ∧ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = (𝐹𝑥))
432199ffvelrni 6845 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
43344, 432syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐺 supp ∅))
434197, 433sseldd 3971 . . . . . . . . . . . 12 (𝜑 → (𝑂 dom 𝑂) ∈ 𝐵)
435 onelon 6213 . . . . . . . . . . . 12 ((𝐵 ∈ On ∧ (𝑂 dom 𝑂) ∈ 𝐵) → (𝑂 dom 𝑂) ∈ On)
43610, 434, 435syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) ∈ On)
437436adantr 481 . . . . . . . . . 10 ((𝜑𝑥𝐵) → (𝑂 dom 𝑂) ∈ On)
438 ontri1 6222 . . . . . . . . . 10 ((𝑥 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
439224, 437, 438syl2anc 584 . . . . . . . . 9 ((𝜑𝑥𝐵) → (𝑥 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑥))
440439con2bid 356 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)))
441 simprl 767 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥𝐵)
442377adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)))
443 eloni 6198 . . . . . . . . . . . . . . . . . 18 ((𝑂𝑋) ∈ On → Ord (𝑂𝑋))
444129, 443syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → Ord (𝑂𝑋))
445 orduni 7500 . . . . . . . . . . . . . . . . . 18 (Ord dom 𝑂 → Ord dom 𝑂)
44636, 445ax-mp 5 . . . . . . . . . . . . . . . . 17 Ord dom 𝑂
447 ordtri1 6221 . . . . . . . . . . . . . . . . 17 ((Ord (𝑂𝑋) ∧ Ord dom 𝑂) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
448444, 446, 447sylancl 586 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
44954, 448mpbid 233 . . . . . . . . . . . . . . 15 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
450 isorel 7074 . . . . . . . . . . . . . . . . . 18 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
45146, 44, 52, 450syl12anc 834 . . . . . . . . . . . . . . . . 17 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
452 fvex 6679 . . . . . . . . . . . . . . . . . 18 (𝑂𝑋) ∈ V
453452epeli 5466 . . . . . . . . . . . . . . . . 17 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
454 fvex 6679 . . . . . . . . . . . . . . . . . 18 (𝑂‘(𝑂𝑋)) ∈ V
455454epeli 5466 . . . . . . . . . . . . . . . . 17 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
456451, 453, 4553bitr3g 314 . . . . . . . . . . . . . . . 16 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
457108eleq2d 2902 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
458456, 457bitrd 280 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
459449, 458mtbid 325 . . . . . . . . . . . . . 14 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
460 onelon 6213 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
46110, 161, 460syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑𝑋 ∈ On)
462 ontri1 6222 . . . . . . . . . . . . . . 15 ((𝑋 ∈ On ∧ (𝑂 dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
463461, 436, 462syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑋 ⊆ (𝑂 dom 𝑂) ↔ ¬ (𝑂 dom 𝑂) ∈ 𝑋))
464459, 463mpbird 258 . . . . . . . . . . . . 13 (𝜑𝑋 ⊆ (𝑂 dom 𝑂))
465464adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂 dom 𝑂))
466 simprr 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝑂 dom 𝑂) ∈ 𝑥)
467224adantrr 713 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
468 ontr2 6235 . . . . . . . . . . . . 13 ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
469461, 467, 468syl2an2r 681 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂 dom 𝑂) ∧ (𝑂 dom 𝑂) ∈ 𝑥) → 𝑋𝑥))
470465, 466, 469mp2and 695 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑋𝑥)
471 eleq2 2905 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑋𝑤𝑋𝑥))
472 fveq2 6666 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
473 fveq2 6666 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → (𝐺𝑤) = (𝐺𝑥))
474472, 473eqeq12d 2841 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → ((𝐹𝑤) = (𝐺𝑤) ↔ (𝐹𝑥) = (𝐺𝑥)))
475471, 474imbi12d 346 . . . . . . . . . . . 12 (𝑤 = 𝑥 → ((𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) ↔ (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
476475rspcv 3621 . . . . . . . . . . 11 (𝑥𝐵 → (∀𝑤𝐵 (𝑋𝑤 → (𝐹𝑤) = (𝐺𝑤)) → (𝑋𝑥 → (𝐹𝑥) = (𝐺𝑥))))
477441, 442, 470, 476syl3c 66 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = (𝐺𝑥))
478466adantr 481 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂 dom 𝑂) ∈ 𝑥)
47946ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
48044ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ dom 𝑂)
48151ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:(𝐺 supp ∅)⟶dom 𝑂)
482 ffvelrn 6844 . . . . . . . . . . . . . . . . . 18 ((𝑂:(𝐺 supp ∅)⟶dom 𝑂𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
483481, 482sylancom 588 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ dom 𝑂)
484 isorel 7074 . . . . . . . . . . . . . . . . 17 ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑥) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
485479, 480, 483, 484syl12anc 834 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 E (𝑂𝑥) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥))))
486269epeli 5466 . . . . . . . . . . . . . . . 16 ( dom 𝑂 E (𝑂𝑥) ↔ dom 𝑂 ∈ (𝑂𝑥))
487271epeli 5466 . . . . . . . . . . . . . . . 16 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)))
488485, 486, 4873bitr3g 314 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥))))
48948ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐺 supp ∅))
490489, 261sylancom 588 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(𝑂𝑥)) = 𝑥)
491490eleq2d 2902 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑥)) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
492488, 491bitrd 280 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ( dom 𝑂 ∈ (𝑂𝑥) ↔ (𝑂 dom 𝑂) ∈ 𝑥))
493478, 492mpbird 258 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → dom 𝑂 ∈ (𝑂𝑥))
494 elssuni 4865 . . . . . . . . . . . . . . 15 ((𝑂𝑥) ∈ dom 𝑂 → (𝑂𝑥) ⊆ dom 𝑂)
495483, 494syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ⊆ dom 𝑂)
49636, 483, 275sylancr 587 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂𝑥) ∈ On)
497496, 277syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (𝑂𝑥))
498 ordtri1 6221 . . . . . . . . . . . . . . 15 ((Ord (𝑂𝑥) ∧ Ord dom 𝑂) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
499497, 446, 498sylancl 586 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂𝑥) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑥)))
500495, 499mpbid 233 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ dom 𝑂 ∈ (𝑂𝑥))
501493, 500pm2.65da 813 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
502441, 501eldifd 3950 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
503 ssidd 3993 . . . . . . . . . . . 12 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
504159, 503, 10, 176suppssr 7855 . . . . . . . . . . 11 ((𝜑𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑥) = ∅)
505502, 504syldan 591 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐺𝑥) = ∅)
506477, 505eqtrd 2860 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵 ∧ (𝑂 dom 𝑂) ∈ 𝑥)) → (𝐹𝑥) = ∅)
507506expr 457 . . . . . . . 8 ((𝜑𝑥𝐵) → ((𝑂 dom 𝑂) ∈ 𝑥 → (𝐹𝑥) = ∅))
508440, 507sylbird 261 . . . . . . 7 ((𝜑𝑥𝐵) → (¬ 𝑥 ⊆ (𝑂 dom 𝑂) → (𝐹𝑥) = ∅))
509508imp 407 . . . . . 6 (((𝜑𝑥𝐵) ∧ ¬ 𝑥 ⊆ (𝑂 dom 𝑂)) → (𝐹𝑥) = ∅)
510429, 430, 431, 509ifbothda 4506 . . . . 5 ((𝜑𝑥𝐵) → (𝐹𝑥) = if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))
511510mpteq2dva 5157 . . . 4 (𝜑 → (𝑥𝐵 ↦ (𝐹𝑥)) = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
512428, 511eqtrd 2860 . . 3 (𝜑𝐹 = (𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅)))
513512fveq2d 6670 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥𝐵 ↦ if(𝑥 ⊆ (𝑂 dom 𝑂), (𝐹𝑥), ∅))))
5148, 9, 10, 2, 13, 113cantnfval 9123 . . 3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
51543fveq2d 6670 . . 3 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
516514, 515eqtrd 2860 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc dom 𝑂))
517427, 513, 5163eltr4d 2932 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 843   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107   ≠ wne 3020  ∀wral 3142  ∃wrex 3143  {crab 3146  Vcvv 3499   ∖ cdif 3936   ⊆ wss 3939  ∅c0 4294  ifcif 4469  ∪ cuni 4836   class class class wbr 5062  {copab 5124   ↦ cmpt 5142  Tr wtr 5168   E cep 5462   We wwe 5511  ◡ccnv 5552  dom cdm 5553  Ord word 6187  Oncon0 6188  Lim wlim 6189  suc csuc 6190  Fun wfun 6345   Fn wfn 6346  ⟶wf 6347  –1-1-onto→wf1o 6350  ‘cfv 6351   Isom wiso 6352  (class class class)co 7151   ∈ cmpo 7153  ωcom 7571   supp csupp 7824  seqωcseqom 8077  1oc1o 8089   +o coa 8093   ·o comu 8094   ↑o coe 8095   ≈ cen 8498   finSupp cfsupp 8825  OrdIsocoi 8965   CNF ccnf 9116 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-seqom 8078  df-1o 8096  df-2o 8097  df-oadd 8100  df-omul 8101  df-oexp 8102  df-er 8282  df-map 8401  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-oi 8966  df-cnf 9117 This theorem is referenced by:  cantnf  9148
 Copyright terms: Public domain W3C validator