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

Theorem cantnfp1lem3 9131
Description: Lemma for cantnfp1 9132. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 1-Jul-2019.)
Hypotheses
Ref Expression
cantnfs.s 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a (𝜑𝐴 ∈ On)
cantnfs.b (𝜑𝐵 ∈ On)
cantnfp1.g (𝜑𝐺𝑆)
cantnfp1.x (𝜑𝑋𝐵)
cantnfp1.y (𝜑𝑌𝐴)
cantnfp1.s (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
cantnfp1.f 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
cantnfp1.e (𝜑 → ∅ ∈ 𝑌)
cantnfp1.o 𝑂 = OrdIso( E , (𝐹 supp ∅))
cantnfp1.h 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝑂𝑘)) ·o (𝐹‘(𝑂𝑘))) +o 𝑧)), ∅)
cantnfp1.k 𝐾 = OrdIso( E , (𝐺 supp ∅))
cantnfp1.m 𝑀 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐾𝑘)) ·o (𝐺‘(𝐾𝑘))) +o 𝑧)), ∅)
Assertion
Ref Expression
cantnfp1lem3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
Distinct variable groups:   𝑡,𝑘,𝑧,𝐵   𝐴,𝑘,𝑡,𝑧   𝑘,𝐹,𝑧   𝑆,𝑘,𝑡,𝑧   𝑘,𝐺,𝑡,𝑧   𝑘,𝐾,𝑡,𝑧   𝑘,𝑂,𝑧   𝜑,𝑘,𝑡,𝑧   𝑘,𝑌,𝑡,𝑧   𝑘,𝑋,𝑡,𝑧
Allowed substitution hints:   𝐹(𝑡)   𝐻(𝑧,𝑡,𝑘)   𝑀(𝑧,𝑡,𝑘)   𝑂(𝑡)

Proof of Theorem cantnfp1lem3
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cantnfs.s . . 3 𝑆 = dom (𝐴 CNF 𝐵)
2 cantnfs.a . . 3 (𝜑𝐴 ∈ On)
3 cantnfs.b . . 3 (𝜑𝐵 ∈ On)
4 cantnfp1.o . . 3 𝑂 = OrdIso( E , (𝐹 supp ∅))
5 cantnfp1.g . . . 4 (𝜑𝐺𝑆)
6 cantnfp1.x . . . 4 (𝜑𝑋𝐵)
7 cantnfp1.y . . . 4 (𝜑𝑌𝐴)
8 cantnfp1.s . . . 4 (𝜑 → (𝐺 supp ∅) ⊆ 𝑋)
9 cantnfp1.f . . . 4 𝐹 = (𝑡𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)))
101, 2, 3, 5, 6, 7, 8, 9cantnfp1lem1 9129 . . 3 (𝜑𝐹𝑆)
11 cantnfp1.h . . 3 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝑂𝑘)) ·o (𝐹‘(𝑂𝑘))) +o 𝑧)), ∅)
121, 2, 3, 4, 10, 11cantnfval 9119 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂))
13 cantnfp1.e . . . 4 (𝜑 → ∅ ∈ 𝑌)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 9130 . . 3 (𝜑 → dom 𝑂 = suc dom 𝑂)
1514fveq2d 6653 . 2 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
161, 2, 3, 4, 10cantnfcl 9118 . . . . . . 7 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω))
1716simprd 499 . . . . . 6 (𝜑 → dom 𝑂 ∈ ω)
1814, 17eqeltrrd 2894 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
19 peano2b 7580 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
2018, 19sylibr 237 . . . 4 (𝜑 dom 𝑂 ∈ ω)
211, 2, 3, 4, 10, 11cantnfsuc 9121 . . . 4 ((𝜑 dom 𝑂 ∈ ω) → (𝐻‘suc dom 𝑂) = (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)))
2220, 21mpdan 686 . . 3 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)))
23 ovexd 7174 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ∈ V)
2416simpld 498 . . . . . . . . . . . . . . 15 (𝜑 → E We (𝐹 supp ∅))
254oiiso 8989 . . . . . . . . . . . . . . 15 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
2623, 24, 25syl2anc 587 . . . . . . . . . . . . . 14 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
27 isof1o 7059 . . . . . . . . . . . . . 14 (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
2826, 27syl 17 . . . . . . . . . . . . 13 (𝜑𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
29 f1ocnv 6606 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂)
30 f1of 6594 . . . . . . . . . . . . 13 (𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐹 supp ∅)⟶dom 𝑂)
3128, 29, 303syl 18 . . . . . . . . . . . 12 (𝜑𝑂:(𝐹 supp ∅)⟶dom 𝑂)
32 iftrue 4434 . . . . . . . . . . . . . . 15 (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = 𝑌)
339, 32, 6, 7fvmptd3 6772 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑋) = 𝑌)
3413ne0d 4254 . . . . . . . . . . . . . 14 (𝜑𝑌 ≠ ∅)
3533, 34eqnetrd 3057 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑋) ≠ ∅)
367adantr 484 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐵) → 𝑌𝐴)
371, 2, 3cantnfs 9117 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
385, 37mpbid 235 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
3938simpld 498 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺:𝐵𝐴)
4039ffvelrnda 6832 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
4136, 40ifcld 4473 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
4241, 9fmptd 6859 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵𝐴)
4342ffnd 6492 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
44 0ex 5178 . . . . . . . . . . . . . . 15 ∅ ∈ V
4544a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
46 elsuppfn 7825 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
4743, 3, 45, 46syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
486, 35, 47mpbir2and 712 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐹 supp ∅))
4931, 48ffvelrnd 6833 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
50 elssuni 4833 . . . . . . . . . . 11 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5149, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
524oicl 8981 . . . . . . . . . . . 12 Ord dom 𝑂
53 ordelon 6187 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
5452, 49, 53sylancr 590 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
55 nnon 7570 . . . . . . . . . . . 12 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ On)
5620, 55syl 17 . . . . . . . . . . 11 (𝜑 dom 𝑂 ∈ On)
57 ontri1 6197 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ dom 𝑂 ∈ On) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
5854, 56, 57syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
5951, 58mpbid 235 . . . . . . . . 9 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
60 sucidg 6241 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ suc dom 𝑂)
6120, 60syl 17 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
6261, 14eleqtrrd 2896 . . . . . . . . . . . 12 (𝜑 dom 𝑂 ∈ dom 𝑂)
63 isorel 7062 . . . . . . . . . . . 12 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
6426, 62, 49, 63syl12anc 835 . . . . . . . . . . 11 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
65 fvex 6662 . . . . . . . . . . . 12 (𝑂𝑋) ∈ V
6665epeli 5436 . . . . . . . . . . 11 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
67 fvex 6662 . . . . . . . . . . . 12 (𝑂‘(𝑂𝑋)) ∈ V
6867epeli 5436 . . . . . . . . . . 11 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
6964, 66, 683bitr3g 316 . . . . . . . . . 10 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
70 f1ocnvfv2 7016 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
7128, 48, 70syl2anc 587 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
7271eleq2d 2878 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
7369, 72bitrd 282 . . . . . . . . 9 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
7459, 73mtbid 327 . . . . . . . 8 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
758sseld 3917 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → (𝑂 dom 𝑂) ∈ 𝑋))
76 suppssdm 7830 . . . . . . . . . . . . . . . 16 (𝐹 supp ∅) ⊆ dom 𝐹
7776, 42fssdm 6508 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
78 onss 7489 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → 𝐵 ⊆ On)
793, 78syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ On)
8077, 79sstrd 3928 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) ⊆ On)
814oif 8982 . . . . . . . . . . . . . . . 16 𝑂:dom 𝑂⟶(𝐹 supp ∅)
8281ffvelrni 6831 . . . . . . . . . . . . . . 15 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8362, 82syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8480, 83sseldd 3919 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ On)
85 eloni 6173 . . . . . . . . . . . . 13 ((𝑂 dom 𝑂) ∈ On → Ord (𝑂 dom 𝑂))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → Ord (𝑂 dom 𝑂))
87 ordn2lp 6183 . . . . . . . . . . . 12 (Ord (𝑂 dom 𝑂) → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
8886, 87syl 17 . . . . . . . . . . 11 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
89 imnan 403 . . . . . . . . . . 11 (((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)) ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9088, 89sylibr 237 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
9175, 90syld 47 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
92 onelon 6188 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
933, 6, 92syl2anc 587 . . . . . . . . . . . 12 (𝜑𝑋 ∈ On)
94 eloni 6173 . . . . . . . . . . . 12 (𝑋 ∈ On → Ord 𝑋)
9593, 94syl 17 . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
96 ordirr 6181 . . . . . . . . . . 11 (Ord 𝑋 → ¬ 𝑋𝑋)
9795, 96syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑋𝑋)
98 elsni 4545 . . . . . . . . . . . 12 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑂 dom 𝑂) = 𝑋)
9998eleq2d 2878 . . . . . . . . . . 11 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂 dom 𝑂) ↔ 𝑋𝑋))
10099notbid 321 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂 dom 𝑂) ↔ ¬ 𝑋𝑋))
10197, 100syl5ibrcom 250 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
102 eqeq1 2805 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
103 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
104102, 103ifbieq2d 4453 . . . . . . . . . . . . . 14 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
105 eldifi 4057 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
106105adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
1077adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
108 fvex 6662 . . . . . . . . . . . . . . 15 (𝐺𝑘) ∈ V
109 ifexg 4475 . . . . . . . . . . . . . . 15 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
110107, 108, 109sylancl 589 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
1119, 104, 106, 110fvmptd3 6772 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
112 eldifn 4058 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
113112adantl 485 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
114 velsn 4544 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
115 elun2 4107 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
116114, 115sylbir 238 . . . . . . . . . . . . . . 15 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
117113, 116nsyl 142 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
118117iffalsed 4439 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
119 ssun1 4102 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
120 sscon 4069 . . . . . . . . . . . . . . . 16 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
121119, 120ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
122121sseli 3914 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
123 ssidd 3941 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
12439, 123, 3, 13suppssr 7848 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
125122, 124sylan2 595 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
126111, 118, 1253eqtrd 2840 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
12742, 126suppss 7847 . . . . . . . . . . 11 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
128127, 83sseldd 3919 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}))
129 elun 4079 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
130128, 129sylib 221 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
13191, 101, 130mpjaod 857 . . . . . . . 8 (𝜑 → ¬ 𝑋 ∈ (𝑂 dom 𝑂))
132 ioran 981 . . . . . . . 8 (¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)) ↔ (¬ (𝑂 dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
13374, 131, 132sylanbrc 586 . . . . . . 7 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
134 ordtri3 6199 . . . . . . . 8 ((Ord (𝑂 dom 𝑂) ∧ Ord 𝑋) → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
13586, 95, 134syl2anc 587 . . . . . . 7 (𝜑 → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
136133, 135mpbird 260 . . . . . 6 (𝜑 → (𝑂 dom 𝑂) = 𝑋)
137136oveq2d 7155 . . . . 5 (𝜑 → (𝐴o (𝑂 dom 𝑂)) = (𝐴o 𝑋))
138136fveq2d 6653 . . . . . 6 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = (𝐹𝑋))
139138, 33eqtrd 2836 . . . . 5 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = 𝑌)
140137, 139oveq12d 7157 . . . 4 (𝜑 → ((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) = ((𝐴o 𝑋) ·o 𝑌))
141 nnord 7572 . . . . . . . . 9 ( dom 𝑂 ∈ ω → Ord dom 𝑂)
14220, 141syl 17 . . . . . . . 8 (𝜑 → Ord dom 𝑂)
143 sssucid 6240 . . . . . . . . . 10 dom 𝑂 ⊆ suc dom 𝑂
144143, 14sseqtrrid 3971 . . . . . . . . 9 (𝜑 dom 𝑂 ⊆ dom 𝑂)
145 f1ofo 6601 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂onto→(𝐹 supp ∅))
14628, 145syl 17 . . . . . . . . . . . 12 (𝜑𝑂:dom 𝑂onto→(𝐹 supp ∅))
147 foima 6574 . . . . . . . . . . . 12 (𝑂:dom 𝑂onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
148146, 147syl 17 . . . . . . . . . . 11 (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
149 ffn 6491 . . . . . . . . . . . . . 14 (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂)
15081, 149ax-mp 5 . . . . . . . . . . . . 13 𝑂 Fn dom 𝑂
151 fnsnfv 6722 . . . . . . . . . . . . 13 ((𝑂 Fn dom 𝑂 dom 𝑂 ∈ dom 𝑂) → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
152150, 62, 151sylancr 590 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
153136sneqd 4540 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = {𝑋})
154152, 153eqtr3d 2838 . . . . . . . . . . 11 (𝜑 → (𝑂 “ { dom 𝑂}) = {𝑋})
155148, 154difeq12d 4054 . . . . . . . . . 10 (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})) = ((𝐹 supp ∅) ∖ {𝑋}))
156 ordirr 6181 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → ¬ dom 𝑂 dom 𝑂)
157142, 156syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ dom 𝑂 dom 𝑂)
158 disjsn 4610 . . . . . . . . . . . . . . . 16 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ ¬ dom 𝑂 dom 𝑂)
159157, 158sylibr 237 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∩ { dom 𝑂}) = ∅)
160 disj3 4364 . . . . . . . . . . . . . . 15 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
161159, 160sylib 221 . . . . . . . . . . . . . 14 (𝜑 dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
162 difun2 4390 . . . . . . . . . . . . . 14 (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}) = ( dom 𝑂 ∖ { dom 𝑂})
163161, 162eqtr4di 2854 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
164 df-suc 6169 . . . . . . . . . . . . . . 15 suc dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂})
16514, 164eqtrdi 2852 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂}))
166165difeq1d 4052 . . . . . . . . . . . . 13 (𝜑 → (dom 𝑂 ∖ { dom 𝑂}) = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
167163, 166eqtr4d 2839 . . . . . . . . . . . 12 (𝜑 dom 𝑂 = (dom 𝑂 ∖ { dom 𝑂}))
168167imaeq2d 5900 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) = (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})))
169 dff1o3 6600 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂onto→(𝐹 supp ∅) ∧ Fun 𝑂))
170169simprbi 500 . . . . . . . . . . . 12 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → Fun 𝑂)
171 imadif 6412 . . . . . . . . . . . 12 (Fun 𝑂 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
17228, 170, 1713syl 18 . . . . . . . . . . 11 (𝜑 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
173168, 172eqtrd 2836 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
1748, 97ssneldd 3921 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅))
175 disjsn 4610 . . . . . . . . . . . . 13 (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅))
176174, 175sylibr 237 . . . . . . . . . . . 12 (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅)
177 fvex 6662 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑋) ∈ V
178 dif1o 8112 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑋) ∈ (V ∖ 1o) ↔ ((𝐺𝑋) ∈ V ∧ (𝐺𝑋) ≠ ∅))
179177, 178mpbiran 708 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑋) ∈ (V ∖ 1o) ↔ (𝐺𝑋) ≠ ∅)
18039ffnd 6492 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn 𝐵)
181 elsuppfn 7825 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
182180, 3, 45, 181syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
183179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1o) ↔ (𝐺𝑋) ≠ ∅))
184183bicomd 226 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐺𝑋) ≠ ∅ ↔ (𝐺𝑋) ∈ (V ∖ 1o)))
185184anbi2d 631 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o))))
186182, 185bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o))))
1878sseld 3917 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋𝑋))
188186, 187sylbird 263 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o)) → 𝑋𝑋))
1896, 188mpand 694 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1o) → 𝑋𝑋))
190179, 189syl5bir 246 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑋) ≠ ∅ → 𝑋𝑋))
191190necon1bd 3008 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑋𝑋 → (𝐺𝑋) = ∅))
19297, 191mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑋) = ∅)
193192adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑋) = ∅)
194 fveqeq2 6658 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑋 → ((𝐺𝑘) = ∅ ↔ (𝐺𝑋) = ∅))
195193, 194syl5ibrcom 250 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺𝑘) = ∅))
196 eldifi 4057 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘𝐵)
197196adantl 485 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘𝐵)
1987adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌𝐴)
199198, 108, 109sylancl 589 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
2009, 104, 197, 199fvmptd3 6772 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
201 ssidd 3941 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
20242, 201, 3, 13suppssr 7848 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = ∅)
203200, 202eqtr3d 2838 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅)
204 iffalse 4437 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
205204eqeq1d 2803 . . . . . . . . . . . . . . . 16 𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅ ↔ (𝐺𝑘) = ∅))
206203, 205syl5ibcom 248 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺𝑘) = ∅))
207195, 206pm2.61d 182 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑘) = ∅)
20839, 207suppss 7847 . . . . . . . . . . . . 13 (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅))
209 reldisj 4362 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
210208, 209syl 17 . . . . . . . . . . . 12 (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
211176, 210mpbid 235 . . . . . . . . . . 11 (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))
212 uncom 4083 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅))
213127, 212sseqtrdi 3968 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)))
214 ssundif 4394 . . . . . . . . . . . 12 ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
215213, 214sylib 221 . . . . . . . . . . 11 (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
216211, 215eqssd 3935 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋}))
217155, 173, 2163eqtr4rd 2847 . . . . . . . . 9 (𝜑 → (𝐺 supp ∅) = (𝑂 dom 𝑂))
218 isores3 7071 . . . . . . . . 9 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 dom 𝑂)) → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
21926, 144, 217, 218syl3anc 1368 . . . . . . . 8 (𝜑 → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
220 cantnfp1.k . . . . . . . . . . 11 𝐾 = OrdIso( E , (𝐺 supp ∅))
2211, 2, 3, 220, 5cantnfcl 9118 . . . . . . . . . 10 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω))
222221simpld 498 . . . . . . . . 9 (𝜑 → E We (𝐺 supp ∅))
223 epse 5506 . . . . . . . . 9 E Se (𝐺 supp ∅)
224220oieu 8991 . . . . . . . . 9 (( E We (𝐺 supp ∅) ∧ E Se (𝐺 supp ∅)) → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
225222, 223, 224sylancl 589 . . . . . . . 8 (𝜑 → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
226142, 219, 225mpbi2and 711 . . . . . . 7 (𝜑 → ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾))
227226simpld 498 . . . . . 6 (𝜑 dom 𝑂 = dom 𝐾)
228227fveq2d 6653 . . . . 5 (𝜑 → (𝑀 dom 𝑂) = (𝑀‘dom 𝐾))
229 eleq1 2880 . . . . . . . . . 10 (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
230 fveq2 6649 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
231 fveq2 6649 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
232 cantnfp1.m . . . . . . . . . . . . . 14 𝑀 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐾𝑘)) ·o (𝐺‘(𝐾𝑘))) +o 𝑧)), ∅)
233232seqom0g 8079 . . . . . . . . . . . . 13 (∅ ∈ V → (𝑀‘∅) = ∅)
23444, 233ax-mp 5 . . . . . . . . . . . 12 (𝑀‘∅) = ∅
235231, 234eqtrdi 2852 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑀𝑥) = ∅)
236230, 235eqeq12d 2817 . . . . . . . . . 10 (𝑥 = ∅ → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘∅) = ∅))
237229, 236imbi12d 348 . . . . . . . . 9 (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)))
238237imbi2d 344 . . . . . . . 8 (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))))
239 eleq1 2880 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
240 fveq2 6649 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
241 fveq2 6649 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
242240, 241eqeq12d 2817 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻𝑦) = (𝑀𝑦)))
243239, 242imbi12d 348 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
244243imbi2d 344 . . . . . . . 8 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)))))
245 eleq1 2880 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂))
246 fveq2 6649 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
247 fveq2 6649 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑀𝑥) = (𝑀‘suc 𝑦))
248246, 247eqeq12d 2817 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
249245, 248imbi12d 348 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
250249imbi2d 344 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
251 eleq1 2880 . . . . . . . . . 10 (𝑥 = dom 𝑂 → (𝑥 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
252 fveq2 6649 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝐻𝑥) = (𝐻 dom 𝑂))
253 fveq2 6649 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝑀𝑥) = (𝑀 dom 𝑂))
254252, 253eqeq12d 2817 . . . . . . . . . 10 (𝑥 = dom 𝑂 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
255251, 254imbi12d 348 . . . . . . . . 9 (𝑥 = dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
256255imbi2d 344 . . . . . . . 8 (𝑥 = dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))))
25711seqom0g 8079 . . . . . . . . 9 (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)
258257a1i 11 . . . . . . . 8 (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))
259 nnord 7572 . . . . . . . . . . . . . . . 16 (dom 𝑂 ∈ ω → Ord dom 𝑂)
26017, 259syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Ord dom 𝑂)
261 ordtr 6177 . . . . . . . . . . . . . . 15 (Ord dom 𝑂 → Tr dom 𝑂)
262260, 261syl 17 . . . . . . . . . . . . . 14 (𝜑 → Tr dom 𝑂)
263 trsuc 6247 . . . . . . . . . . . . . 14 ((Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
264262, 263sylan 583 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
265264ex 416 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
266265imim1d 82 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
267 oveq2 7147 . . . . . . . . . . . . . 14 ((𝐻𝑦) = (𝑀𝑦) → (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
268 elnn 7574 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω)
269268ancoms 462 . . . . . . . . . . . . . . . . 17 ((dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
27017, 264, 269syl2an2r 684 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
2711, 2, 3, 4, 10, 11cantnfsuc 9121 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)))
272270, 271syldan 594 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)))
2731, 2, 3, 220, 5, 232cantnfsuc 9121 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)))
274270, 273syldan 594 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)))
275226simprd 499 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑂 dom 𝑂) = 𝐾)
276275fveq1d 6651 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
277276adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
27814eleq2d 2878 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
279278biimpa 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc dom 𝑂)
280142adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord dom 𝑂)
281 ordsucelsuc 7521 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord dom 𝑂 → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
283279, 282mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 dom 𝑂)
284283fvresd 6669 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
285277, 284eqtr3d 2838 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) = (𝑂𝑦))
286285oveq2d 7155 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴o (𝐾𝑦)) = (𝐴o (𝑂𝑦)))
287 eqeq1 2805 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → (𝑡 = 𝑋 ↔ (𝐾𝑦) = 𝑋))
288 fveq2 6649 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → (𝐺𝑡) = (𝐺‘(𝐾𝑦)))
289287, 288ifbieq2d 4453 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
290 suppssdm 7830 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
291290, 39fssdm 6508 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
292291adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵)
293227adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → dom 𝑂 = dom 𝐾)
294283, 293eleqtrd 2895 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾)
295220oif 8982 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾:dom 𝐾⟶(𝐺 supp ∅)
296295ffvelrni 6831 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ dom 𝐾 → (𝐾𝑦) ∈ (𝐺 supp ∅))
297294, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ (𝐺 supp ∅))
298292, 297sseldd 3919 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ 𝐵)
2997adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌𝐴)
300 fvex 6662 . . . . . . . . . . . . . . . . . . . . 21 (𝐺‘(𝐾𝑦)) ∈ V
301 ifexg 4475 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ (𝐺‘(𝐾𝑦)) ∈ V) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
302299, 300, 301sylancl 589 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
3039, 289, 298, 302fvmptd3 6772 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
304285fveq2d 6653 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
305174adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅))
306 nelneq 2917 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾𝑦) = 𝑋)
307297, 305, 306syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾𝑦) = 𝑋)
308307iffalsed 4439 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) = (𝐺‘(𝐾𝑦)))
309303, 304, 3083eqtr3rd 2845 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
310286, 309oveq12d 7157 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) = ((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))))
311310oveq1d 7154 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
312274, 311eqtrd 2836 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
313272, 312eqeq12d 2817 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦))))
314267, 313syl5ibr 249 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
315314ex 416 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
316315a2d 29 . . . . . . . . . . 11 (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
317266, 316syld 47 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
318317a2i 14 . . . . . . . . 9 ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
319318a1i 11 . . . . . . . 8 (𝑦 ∈ ω → ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
320238, 244, 250, 256, 258, 319finds 7593 . . . . . . 7 ( dom 𝑂 ∈ ω → (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
32120, 320mpcom 38 . . . . . 6 (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
32262, 321mpd 15 . . . . 5 (𝜑 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))
3231, 2, 3, 220, 5, 232cantnfval 9119 . . . . 5 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾))
324228, 322, 3233eqtr4d 2846 . . . 4 (𝜑 → (𝐻 dom 𝑂) = ((𝐴 CNF 𝐵)‘𝐺))
325140, 324oveq12d 7157 . . 3 (𝜑 → (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
32622, 325eqtrd 2836 . 2 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
32712, 15, 3263eqtrd 2840 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wcel 2112  wne 2990  Vcvv 3444  cdif 3881  cun 3882  cin 3883  wss 3884  c0 4246  ifcif 4428  {csn 4528   cuni 4803   class class class wbr 5033  cmpt 5113  Tr wtr 5139   E cep 5432   Se wse 5480   We wwe 5481  ccnv 5522  dom cdm 5523  cres 5525  cima 5526  Ord word 6162  Oncon0 6163  suc csuc 6165  Fun wfun 6322   Fn wfn 6323  wf 6324  ontowfo 6326  1-1-ontowf1o 6327  cfv 6328   Isom wiso 6329  (class class class)co 7139  cmpo 7141  ωcom 7564   supp csupp 7817  seqωcseqom 8070  1oc1o 8082   +o coa 8086   ·o comu 8087  o coe 8088   finSupp cfsupp 8821  OrdIsocoi 8961   CNF ccnf 9112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-om 7565  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-seqom 8071  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-oi 8962  df-cnf 9113
This theorem is referenced by:  cantnfp1  9132
  Copyright terms: Public domain W3C validator