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

Theorem cantnfp1lem3 9718
Description: Lemma for cantnfp1 9719. (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 9716 . . 3 (𝜑𝐹𝑆)
11 cantnfp1.h . . 3 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝑂𝑘)) ·o (𝐹‘(𝑂𝑘))) +o 𝑧)), ∅)
121, 2, 3, 4, 10, 11cantnfval 9706 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂))
13 cantnfp1.e . . . 4 (𝜑 → ∅ ∈ 𝑌)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 9717 . . 3 (𝜑 → dom 𝑂 = suc dom 𝑂)
1514fveq2d 6911 . 2 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
161, 2, 3, 4, 10cantnfcl 9705 . . . . . . 7 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω))
1716simprd 495 . . . . . 6 (𝜑 → dom 𝑂 ∈ ω)
1814, 17eqeltrrd 2840 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
19 peano2b 7904 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
2018, 19sylibr 234 . . . 4 (𝜑 dom 𝑂 ∈ ω)
211, 2, 3, 4, 10, 11cantnfsuc 9708 . . . 4 ((𝜑 dom 𝑂 ∈ ω) → (𝐻‘suc dom 𝑂) = (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)))
2220, 21mpdan 687 . . 3 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)))
23 ovexd 7466 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ∈ V)
2416simpld 494 . . . . . . . . . . . . . . 15 (𝜑 → E We (𝐹 supp ∅))
254oiiso 9575 . . . . . . . . . . . . . . 15 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
2623, 24, 25syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
27 isof1o 7343 . . . . . . . . . . . . . 14 (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
2826, 27syl 17 . . . . . . . . . . . . 13 (𝜑𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
29 f1ocnv 6861 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂)
30 f1of 6849 . . . . . . . . . . . . 13 (𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐹 supp ∅)⟶dom 𝑂)
3128, 29, 303syl 18 . . . . . . . . . . . 12 (𝜑𝑂:(𝐹 supp ∅)⟶dom 𝑂)
32 iftrue 4537 . . . . . . . . . . . . . . 15 (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = 𝑌)
339, 32, 6, 7fvmptd3 7039 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑋) = 𝑌)
3413ne0d 4348 . . . . . . . . . . . . . 14 (𝜑𝑌 ≠ ∅)
3533, 34eqnetrd 3006 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑋) ≠ ∅)
367adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐵) → 𝑌𝐴)
371, 2, 3cantnfs 9704 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
385, 37mpbid 232 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
3938simpld 494 . . . . . . . . . . . . . . . . . 18 (𝜑𝐺:𝐵𝐴)
4039ffvelcdmda 7104 . . . . . . . . . . . . . . . . 17 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
4136, 40ifcld 4577 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
4241, 9fmptd 7134 . . . . . . . . . . . . . . 15 (𝜑𝐹:𝐵𝐴)
4342ffnd 6738 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
44 0ex 5313 . . . . . . . . . . . . . . 15 ∅ ∈ V
4544a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
46 elsuppfn 8194 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
4743, 3, 45, 46syl3anc 1370 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
486, 35, 47mpbir2and 713 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐹 supp ∅))
4931, 48ffvelcdmd 7105 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
50 elssuni 4942 . . . . . . . . . . 11 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5149, 50syl 17 . . . . . . . . . 10 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
524oicl 9567 . . . . . . . . . . . 12 Ord dom 𝑂
53 ordelon 6410 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
5452, 49, 53sylancr 587 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
55 nnon 7893 . . . . . . . . . . . 12 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ On)
5620, 55syl 17 . . . . . . . . . . 11 (𝜑 dom 𝑂 ∈ On)
57 ontri1 6420 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ dom 𝑂 ∈ On) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
5854, 56, 57syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
5951, 58mpbid 232 . . . . . . . . 9 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
60 sucidg 6467 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ suc dom 𝑂)
6120, 60syl 17 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
6261, 14eleqtrrd 2842 . . . . . . . . . . . 12 (𝜑 dom 𝑂 ∈ dom 𝑂)
63 isorel 7346 . . . . . . . . . . . 12 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
6426, 62, 49, 63syl12anc 837 . . . . . . . . . . 11 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
65 fvex 6920 . . . . . . . . . . . 12 (𝑂𝑋) ∈ V
6665epeli 5591 . . . . . . . . . . 11 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
67 fvex 6920 . . . . . . . . . . . 12 (𝑂‘(𝑂𝑋)) ∈ V
6867epeli 5591 . . . . . . . . . . 11 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
6964, 66, 683bitr3g 313 . . . . . . . . . 10 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
70 f1ocnvfv2 7297 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
7128, 48, 70syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
7271eleq2d 2825 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
7369, 72bitrd 279 . . . . . . . . 9 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
7459, 73mtbid 324 . . . . . . . 8 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
758sseld 3994 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → (𝑂 dom 𝑂) ∈ 𝑋))
76 suppssdm 8201 . . . . . . . . . . . . . . . 16 (𝐹 supp ∅) ⊆ dom 𝐹
7776, 42fssdm 6756 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
78 onss 7804 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → 𝐵 ⊆ On)
793, 78syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ On)
8077, 79sstrd 4006 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) ⊆ On)
814oif 9568 . . . . . . . . . . . . . . . 16 𝑂:dom 𝑂⟶(𝐹 supp ∅)
8281ffvelcdmi 7103 . . . . . . . . . . . . . . 15 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8362, 82syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8480, 83sseldd 3996 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ On)
85 eloni 6396 . . . . . . . . . . . . 13 ((𝑂 dom 𝑂) ∈ On → Ord (𝑂 dom 𝑂))
8684, 85syl 17 . . . . . . . . . . . 12 (𝜑 → Ord (𝑂 dom 𝑂))
87 ordn2lp 6406 . . . . . . . . . . . 12 (Ord (𝑂 dom 𝑂) → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
8886, 87syl 17 . . . . . . . . . . 11 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
89 imnan 399 . . . . . . . . . . 11 (((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)) ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9088, 89sylibr 234 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
9175, 90syld 47 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
92 onelon 6411 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
933, 6, 92syl2anc 584 . . . . . . . . . . . 12 (𝜑𝑋 ∈ On)
94 eloni 6396 . . . . . . . . . . . 12 (𝑋 ∈ On → Ord 𝑋)
9593, 94syl 17 . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
96 ordirr 6404 . . . . . . . . . . 11 (Ord 𝑋 → ¬ 𝑋𝑋)
9795, 96syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑋𝑋)
98 elsni 4648 . . . . . . . . . . . 12 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑂 dom 𝑂) = 𝑋)
9998eleq2d 2825 . . . . . . . . . . 11 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂 dom 𝑂) ↔ 𝑋𝑋))
10099notbid 318 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂 dom 𝑂) ↔ ¬ 𝑋𝑋))
10197, 100syl5ibrcom 247 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
102 eqeq1 2739 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
103 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
104102, 103ifbieq2d 4557 . . . . . . . . . . . . . 14 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
105 eldifi 4141 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
106105adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
1077adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
108 fvex 6920 . . . . . . . . . . . . . . 15 (𝐺𝑘) ∈ V
109 ifexg 4580 . . . . . . . . . . . . . . 15 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
110107, 108, 109sylancl 586 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
1119, 104, 106, 110fvmptd3 7039 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
112 eldifn 4142 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
113112adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
114 velsn 4647 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
115 elun2 4193 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
116114, 115sylbir 235 . . . . . . . . . . . . . . 15 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
117113, 116nsyl 140 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
118117iffalsed 4542 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
119 ssun1 4188 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
120 sscon 4153 . . . . . . . . . . . . . . . 16 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
121119, 120ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
122121sseli 3991 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
123 ssidd 4019 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
12439, 123, 3, 13suppssr 8219 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
125122, 124sylan2 593 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
126111, 118, 1253eqtrd 2779 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
12742, 126suppss 8218 . . . . . . . . . . 11 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
128127, 83sseldd 3996 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}))
129 elun 4163 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
130128, 129sylib 218 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
13191, 101, 130mpjaod 860 . . . . . . . 8 (𝜑 → ¬ 𝑋 ∈ (𝑂 dom 𝑂))
132 ioran 985 . . . . . . . 8 (¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)) ↔ (¬ (𝑂 dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
13374, 131, 132sylanbrc 583 . . . . . . 7 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
134 ordtri3 6422 . . . . . . . 8 ((Ord (𝑂 dom 𝑂) ∧ Ord 𝑋) → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
13586, 95, 134syl2anc 584 . . . . . . 7 (𝜑 → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
136133, 135mpbird 257 . . . . . 6 (𝜑 → (𝑂 dom 𝑂) = 𝑋)
137136oveq2d 7447 . . . . 5 (𝜑 → (𝐴o (𝑂 dom 𝑂)) = (𝐴o 𝑋))
138136fveq2d 6911 . . . . . 6 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = (𝐹𝑋))
139138, 33eqtrd 2775 . . . . 5 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = 𝑌)
140137, 139oveq12d 7449 . . . 4 (𝜑 → ((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) = ((𝐴o 𝑋) ·o 𝑌))
141 nnord 7895 . . . . . . . . 9 ( dom 𝑂 ∈ ω → Ord dom 𝑂)
14220, 141syl 17 . . . . . . . 8 (𝜑 → Ord dom 𝑂)
143 sssucid 6466 . . . . . . . . . 10 dom 𝑂 ⊆ suc dom 𝑂
144143, 14sseqtrrid 4049 . . . . . . . . 9 (𝜑 dom 𝑂 ⊆ dom 𝑂)
145 f1ofo 6856 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂onto→(𝐹 supp ∅))
14628, 145syl 17 . . . . . . . . . . . 12 (𝜑𝑂:dom 𝑂onto→(𝐹 supp ∅))
147 foima 6826 . . . . . . . . . . . 12 (𝑂:dom 𝑂onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
148146, 147syl 17 . . . . . . . . . . 11 (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
149 ffn 6737 . . . . . . . . . . . . . 14 (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂)
15081, 149ax-mp 5 . . . . . . . . . . . . 13 𝑂 Fn dom 𝑂
151 fnsnfv 6988 . . . . . . . . . . . . 13 ((𝑂 Fn dom 𝑂 dom 𝑂 ∈ dom 𝑂) → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
152150, 62, 151sylancr 587 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
153136sneqd 4643 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = {𝑋})
154152, 153eqtr3d 2777 . . . . . . . . . . 11 (𝜑 → (𝑂 “ { dom 𝑂}) = {𝑋})
155148, 154difeq12d 4137 . . . . . . . . . 10 (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})) = ((𝐹 supp ∅) ∖ {𝑋}))
156 ordirr 6404 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → ¬ dom 𝑂 dom 𝑂)
157142, 156syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ dom 𝑂 dom 𝑂)
158 disjsn 4716 . . . . . . . . . . . . . . . 16 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ ¬ dom 𝑂 dom 𝑂)
159157, 158sylibr 234 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∩ { dom 𝑂}) = ∅)
160 disj3 4460 . . . . . . . . . . . . . . 15 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
161159, 160sylib 218 . . . . . . . . . . . . . 14 (𝜑 dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
162 difun2 4487 . . . . . . . . . . . . . 14 (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}) = ( dom 𝑂 ∖ { dom 𝑂})
163161, 162eqtr4di 2793 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
164 df-suc 6392 . . . . . . . . . . . . . . 15 suc dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂})
16514, 164eqtrdi 2791 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂}))
166165difeq1d 4135 . . . . . . . . . . . . 13 (𝜑 → (dom 𝑂 ∖ { dom 𝑂}) = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
167163, 166eqtr4d 2778 . . . . . . . . . . . 12 (𝜑 dom 𝑂 = (dom 𝑂 ∖ { dom 𝑂}))
168167imaeq2d 6080 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) = (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})))
169 dff1o3 6855 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂onto→(𝐹 supp ∅) ∧ Fun 𝑂))
170169simprbi 496 . . . . . . . . . . . 12 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → Fun 𝑂)
171 imadif 6652 . . . . . . . . . . . 12 (Fun 𝑂 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
17228, 170, 1713syl 18 . . . . . . . . . . 11 (𝜑 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
173168, 172eqtrd 2775 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
1748, 97ssneldd 3998 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅))
175 disjsn 4716 . . . . . . . . . . . . 13 (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅))
176174, 175sylibr 234 . . . . . . . . . . . 12 (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅)
177 fvex 6920 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑋) ∈ V
178 dif1o 8537 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑋) ∈ (V ∖ 1o) ↔ ((𝐺𝑋) ∈ V ∧ (𝐺𝑋) ≠ ∅))
179177, 178mpbiran 709 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑋) ∈ (V ∖ 1o) ↔ (𝐺𝑋) ≠ ∅)
18039ffnd 6738 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn 𝐵)
181 elsuppfn 8194 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
182180, 3, 45, 181syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
183179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1o) ↔ (𝐺𝑋) ≠ ∅))
184183bicomd 223 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐺𝑋) ≠ ∅ ↔ (𝐺𝑋) ∈ (V ∖ 1o)))
185184anbi2d 630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o))))
186182, 185bitrd 279 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o))))
1878sseld 3994 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋𝑋))
188186, 187sylbird 260 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1o)) → 𝑋𝑋))
1896, 188mpand 695 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1o) → 𝑋𝑋))
190179, 189biimtrrid 243 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑋) ≠ ∅ → 𝑋𝑋))
191190necon1bd 2956 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑋𝑋 → (𝐺𝑋) = ∅))
19297, 191mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑋) = ∅)
193192adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑋) = ∅)
194 fveqeq2 6916 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑋 → ((𝐺𝑘) = ∅ ↔ (𝐺𝑋) = ∅))
195193, 194syl5ibrcom 247 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺𝑘) = ∅))
196 eldifi 4141 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘𝐵)
197196adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘𝐵)
1987adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌𝐴)
199198, 108, 109sylancl 586 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
2009, 104, 197, 199fvmptd3 7039 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
201 ssidd 4019 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
20242, 201, 3, 13suppssr 8219 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = ∅)
203200, 202eqtr3d 2777 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅)
204 iffalse 4540 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
205204eqeq1d 2737 . . . . . . . . . . . . . . . 16 𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅ ↔ (𝐺𝑘) = ∅))
206203, 205syl5ibcom 245 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺𝑘) = ∅))
207195, 206pm2.61d 179 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑘) = ∅)
20839, 207suppss 8218 . . . . . . . . . . . . 13 (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅))
209 reldisj 4459 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
210208, 209syl 17 . . . . . . . . . . . 12 (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
211176, 210mpbid 232 . . . . . . . . . . 11 (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))
212 uncom 4168 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅))
213127, 212sseqtrdi 4046 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)))
214 ssundif 4494 . . . . . . . . . . . 12 ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
215213, 214sylib 218 . . . . . . . . . . 11 (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
216211, 215eqssd 4013 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋}))
217155, 173, 2163eqtr4rd 2786 . . . . . . . . 9 (𝜑 → (𝐺 supp ∅) = (𝑂 dom 𝑂))
218 isores3 7355 . . . . . . . . 9 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 dom 𝑂)) → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
21926, 144, 217, 218syl3anc 1370 . . . . . . . 8 (𝜑 → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
220 cantnfp1.k . . . . . . . . . . 11 𝐾 = OrdIso( E , (𝐺 supp ∅))
2211, 2, 3, 220, 5cantnfcl 9705 . . . . . . . . . 10 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω))
222221simpld 494 . . . . . . . . 9 (𝜑 → E We (𝐺 supp ∅))
223 epse 5671 . . . . . . . . 9 E Se (𝐺 supp ∅)
224220oieu 9577 . . . . . . . . 9 (( E We (𝐺 supp ∅) ∧ E Se (𝐺 supp ∅)) → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
225222, 223, 224sylancl 586 . . . . . . . 8 (𝜑 → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
226142, 219, 225mpbi2and 712 . . . . . . 7 (𝜑 → ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾))
227226simpld 494 . . . . . 6 (𝜑 dom 𝑂 = dom 𝐾)
228227fveq2d 6911 . . . . 5 (𝜑 → (𝑀 dom 𝑂) = (𝑀‘dom 𝐾))
229 eleq1 2827 . . . . . . . . . 10 (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
230 fveq2 6907 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
231 fveq2 6907 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
232 cantnfp1.m . . . . . . . . . . . . . 14 𝑀 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴o (𝐾𝑘)) ·o (𝐺‘(𝐾𝑘))) +o 𝑧)), ∅)
233232seqom0g 8495 . . . . . . . . . . . . 13 (∅ ∈ V → (𝑀‘∅) = ∅)
23444, 233ax-mp 5 . . . . . . . . . . . 12 (𝑀‘∅) = ∅
235231, 234eqtrdi 2791 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑀𝑥) = ∅)
236230, 235eqeq12d 2751 . . . . . . . . . 10 (𝑥 = ∅ → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘∅) = ∅))
237229, 236imbi12d 344 . . . . . . . . 9 (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)))
238237imbi2d 340 . . . . . . . 8 (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))))
239 eleq1 2827 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
240 fveq2 6907 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
241 fveq2 6907 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
242240, 241eqeq12d 2751 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻𝑦) = (𝑀𝑦)))
243239, 242imbi12d 344 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
244243imbi2d 340 . . . . . . . 8 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)))))
245 eleq1 2827 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂))
246 fveq2 6907 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
247 fveq2 6907 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑀𝑥) = (𝑀‘suc 𝑦))
248246, 247eqeq12d 2751 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
249245, 248imbi12d 344 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
250249imbi2d 340 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
251 eleq1 2827 . . . . . . . . . 10 (𝑥 = dom 𝑂 → (𝑥 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
252 fveq2 6907 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝐻𝑥) = (𝐻 dom 𝑂))
253 fveq2 6907 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝑀𝑥) = (𝑀 dom 𝑂))
254252, 253eqeq12d 2751 . . . . . . . . . 10 (𝑥 = dom 𝑂 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
255251, 254imbi12d 344 . . . . . . . . 9 (𝑥 = dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
256255imbi2d 340 . . . . . . . 8 (𝑥 = dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))))
25711seqom0g 8495 . . . . . . . . 9 (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)
258257a1i 11 . . . . . . . 8 (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))
259 nnord 7895 . . . . . . . . . . . . . . . 16 (dom 𝑂 ∈ ω → Ord dom 𝑂)
26017, 259syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Ord dom 𝑂)
261 ordtr 6400 . . . . . . . . . . . . . . 15 (Ord dom 𝑂 → Tr dom 𝑂)
262260, 261syl 17 . . . . . . . . . . . . . 14 (𝜑 → Tr dom 𝑂)
263 trsuc 6473 . . . . . . . . . . . . . 14 ((Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
264262, 263sylan 580 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
265264ex 412 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
266265imim1d 82 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
267 oveq2 7439 . . . . . . . . . . . . . 14 ((𝐻𝑦) = (𝑀𝑦) → (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
268 elnn 7898 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω)
269268ancoms 458 . . . . . . . . . . . . . . . . 17 ((dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
27017, 264, 269syl2an2r 685 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
2711, 2, 3, 4, 10, 11cantnfsuc 9708 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)))
272270, 271syldan 591 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)))
2731, 2, 3, 220, 5, 232cantnfsuc 9708 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)))
274270, 273syldan 591 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)))
275226simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑂 dom 𝑂) = 𝐾)
276275fveq1d 6909 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
277276adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
27814eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
279278biimpa 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc dom 𝑂)
280142adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord dom 𝑂)
281 ordsucelsuc 7842 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord dom 𝑂 → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
282280, 281syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
283279, 282mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 dom 𝑂)
284283fvresd 6927 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
285277, 284eqtr3d 2777 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) = (𝑂𝑦))
286285oveq2d 7447 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴o (𝐾𝑦)) = (𝐴o (𝑂𝑦)))
287 eqeq1 2739 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → (𝑡 = 𝑋 ↔ (𝐾𝑦) = 𝑋))
288 fveq2 6907 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → (𝐺𝑡) = (𝐺‘(𝐾𝑦)))
289287, 288ifbieq2d 4557 . . . . . . . . . . . . . . . . . . . 20 (𝑡 = (𝐾𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
290 suppssdm 8201 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
291290, 39fssdm 6756 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
292291adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵)
293227adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → dom 𝑂 = dom 𝐾)
294283, 293eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾)
295220oif 9568 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾:dom 𝐾⟶(𝐺 supp ∅)
296295ffvelcdmi 7103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ dom 𝐾 → (𝐾𝑦) ∈ (𝐺 supp ∅))
297294, 296syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ (𝐺 supp ∅))
298292, 297sseldd 3996 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ 𝐵)
2997adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌𝐴)
300 fvex 6920 . . . . . . . . . . . . . . . . . . . . 21 (𝐺‘(𝐾𝑦)) ∈ V
301 ifexg 4580 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ (𝐺‘(𝐾𝑦)) ∈ V) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
302299, 300, 301sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
3039, 289, 298, 302fvmptd3 7039 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
304285fveq2d 6911 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
305174adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅))
306 nelneq 2863 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾𝑦) = 𝑋)
307297, 305, 306syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾𝑦) = 𝑋)
308307iffalsed 4542 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) = (𝐺‘(𝐾𝑦)))
309303, 304, 3083eqtr3rd 2784 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
310286, 309oveq12d 7449 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) = ((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))))
311310oveq1d 7446 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴o (𝐾𝑦)) ·o (𝐺‘(𝐾𝑦))) +o (𝑀𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
312274, 311eqtrd 2775 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦)))
313272, 312eqeq12d 2751 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝐻𝑦)) = (((𝐴o (𝑂𝑦)) ·o (𝐹‘(𝑂𝑦))) +o (𝑀𝑦))))
314267, 313imbitrrid 246 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
315314ex 412 . . . . . . . . . . . 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 7919 . . . . . . 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 9706 . . . . 5 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾))
324228, 322, 3233eqtr4d 2785 . . . 4 (𝜑 → (𝐻 dom 𝑂) = ((𝐴 CNF 𝐵)‘𝐺))
325140, 324oveq12d 7449 . . 3 (𝜑 → (((𝐴o (𝑂 dom 𝑂)) ·o (𝐹‘(𝑂 dom 𝑂))) +o (𝐻 dom 𝑂)) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
32622, 325eqtrd 2775 . 2 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
32712, 15, 3263eqtrd 2779 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847   = wceq 1537  wcel 2106  wne 2938  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  c0 4339  ifcif 4531  {csn 4631   cuni 4912   class class class wbr 5148  cmpt 5231  Tr wtr 5265   E cep 5588   Se wse 5639   We wwe 5640  ccnv 5688  dom cdm 5689  cres 5691  cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388  Fun wfun 6557   Fn wfn 6558  wf 6559  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564  (class class class)co 7431  cmpo 7433  ωcom 7887   supp csupp 8184  seqωcseqom 8486  1oc1o 8498   +o coa 8502   ·o comu 8503  o coe 8504   finSupp cfsupp 9399  OrdIsocoi 9547   CNF ccnf 9699
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-seqom 8487  df-1o 8505  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-oi 9548  df-cnf 9700
This theorem is referenced by:  cantnfp1  9719
  Copyright terms: Public domain W3C validator