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

Theorem cantnfp1lem3 8834
Description: Lemma for cantnfp1 8835. (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 ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐹‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
cantnfp1.k 𝐾 = OrdIso( E , (𝐺 supp ∅))
cantnfp1.m 𝑀 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐾𝑘)) ·𝑜 (𝐺‘(𝐾𝑘))) +𝑜 𝑧)), ∅)
Assertion
Ref Expression
cantnfp1lem3 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 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 8832 . . 3 (𝜑𝐹𝑆)
11 cantnfp1.h . . 3 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐹‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
121, 2, 3, 4, 10, 11cantnfval 8822 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂))
13 cantnfp1.e . . . 4 (𝜑 → ∅ ∈ 𝑌)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 8833 . . 3 (𝜑 → dom 𝑂 = suc dom 𝑂)
1514fveq2d 6422 . 2 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
161, 2, 3, 4, 10cantnfcl 8821 . . . . . . 7 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω))
1716simprd 485 . . . . . 6 (𝜑 → dom 𝑂 ∈ ω)
1814, 17eqeltrrd 2897 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
19 peano2b 7321 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
2018, 19sylibr 225 . . . 4 (𝜑 dom 𝑂 ∈ ω)
211, 2, 3, 4, 10, 11cantnfsuc 8824 . . . 4 ((𝜑 dom 𝑂 ∈ ω) → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
2220, 21mpdan 670 . . 3 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
23 suppssdm 7552 . . . . . . . . . . . . . . . . 17 (𝐹 supp ∅) ⊆ dom 𝐹
247adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝐵) → 𝑌𝐴)
251, 2, 3cantnfs 8820 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
265, 25mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
2726simpld 484 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:𝐵𝐴)
2827ffvelrnda 6591 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
2924, 28ifcld 4335 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
3029, 9fmptd 6616 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:𝐵𝐴)
3123, 30fssdm 6282 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
323, 31ssexd 5013 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ∈ V)
3316simpld 484 . . . . . . . . . . . . . . 15 (𝜑 → E We (𝐹 supp ∅))
344oiiso 8691 . . . . . . . . . . . . . . 15 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
3532, 33, 34syl2anc 575 . . . . . . . . . . . . . 14 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
36 isof1o 6807 . . . . . . . . . . . . . 14 (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
3735, 36syl 17 . . . . . . . . . . . . 13 (𝜑𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
38 f1ocnv 6375 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂)
39 f1of 6363 . . . . . . . . . . . . 13 (𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐹 supp ∅)⟶dom 𝑂)
4037, 38, 393syl 18 . . . . . . . . . . . 12 (𝜑𝑂:(𝐹 supp ∅)⟶dom 𝑂)
41 iftrue 4296 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = 𝑌)
4241, 9fvmptg 6511 . . . . . . . . . . . . . . 15 ((𝑋𝐵𝑌𝐴) → (𝐹𝑋) = 𝑌)
436, 7, 42syl2anc 575 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑋) = 𝑌)
44 onelon 5975 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
452, 7, 44syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ On)
46 on0eln0 6006 . . . . . . . . . . . . . . . 16 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
4745, 46syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
4813, 47mpbid 223 . . . . . . . . . . . . . 14 (𝜑𝑌 ≠ ∅)
4943, 48eqnetrd 3056 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑋) ≠ ∅)
5030ffnd 6267 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
51 0ex 4997 . . . . . . . . . . . . . . 15 ∅ ∈ V
5251a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
53 elsuppfn 7547 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
5450, 3, 52, 53syl3anc 1483 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
556, 49, 54mpbir2and 695 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐹 supp ∅))
5640, 55ffvelrnd 6592 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
57 elssuni 4672 . . . . . . . . . . 11 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
5856, 57syl 17 . . . . . . . . . 10 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
594oicl 8683 . . . . . . . . . . . 12 Ord dom 𝑂
60 ordelon 5974 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
6159, 56, 60sylancr 577 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
62 nnon 7311 . . . . . . . . . . . 12 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ On)
6320, 62syl 17 . . . . . . . . . . 11 (𝜑 dom 𝑂 ∈ On)
64 ontri1 5984 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ dom 𝑂 ∈ On) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6561, 63, 64syl2anc 575 . . . . . . . . . 10 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6658, 65mpbid 223 . . . . . . . . 9 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
67 sucidg 6029 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ suc dom 𝑂)
6820, 67syl 17 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
6968, 14eleqtrrd 2899 . . . . . . . . . . . 12 (𝜑 dom 𝑂 ∈ dom 𝑂)
70 isorel 6810 . . . . . . . . . . . 12 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
7135, 69, 56, 70syl12anc 856 . . . . . . . . . . 11 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
72 fvex 6431 . . . . . . . . . . . 12 (𝑂𝑋) ∈ V
7372epeli 5239 . . . . . . . . . . 11 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
74 fvex 6431 . . . . . . . . . . . 12 (𝑂‘(𝑂𝑋)) ∈ V
7574epeli 5239 . . . . . . . . . . 11 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
7671, 73, 753bitr3g 304 . . . . . . . . . 10 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
77 f1ocnvfv2 6767 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
7837, 55, 77syl2anc 575 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
7978eleq2d 2882 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8076, 79bitrd 270 . . . . . . . . 9 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8166, 80mtbid 315 . . . . . . . 8 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
828sseld 3808 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → (𝑂 dom 𝑂) ∈ 𝑋))
83 onss 7230 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → 𝐵 ⊆ On)
843, 83syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ On)
8531, 84sstrd 3819 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) ⊆ On)
864oif 8684 . . . . . . . . . . . . . . . 16 𝑂:dom 𝑂⟶(𝐹 supp ∅)
8786ffvelrni 6590 . . . . . . . . . . . . . . 15 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8869, 87syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
8985, 88sseldd 3810 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ On)
90 eloni 5960 . . . . . . . . . . . . 13 ((𝑂 dom 𝑂) ∈ On → Ord (𝑂 dom 𝑂))
9189, 90syl 17 . . . . . . . . . . . 12 (𝜑 → Ord (𝑂 dom 𝑂))
92 ordn2lp 5970 . . . . . . . . . . . 12 (Ord (𝑂 dom 𝑂) → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9391, 92syl 17 . . . . . . . . . . 11 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
94 imnan 388 . . . . . . . . . . 11 (((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)) ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9593, 94sylibr 225 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
9682, 95syld 47 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
97 onelon 5975 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
983, 6, 97syl2anc 575 . . . . . . . . . . . 12 (𝜑𝑋 ∈ On)
99 eloni 5960 . . . . . . . . . . . 12 (𝑋 ∈ On → Ord 𝑋)
10098, 99syl 17 . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
101 ordirr 5968 . . . . . . . . . . 11 (Ord 𝑋 → ¬ 𝑋𝑋)
102100, 101syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑋𝑋)
103 elsni 4398 . . . . . . . . . . . 12 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑂 dom 𝑂) = 𝑋)
104103eleq2d 2882 . . . . . . . . . . 11 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂 dom 𝑂) ↔ 𝑋𝑋))
105104notbid 309 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂 dom 𝑂) ↔ ¬ 𝑋𝑋))
106102, 105syl5ibrcom 238 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
107 eldifi 3942 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
108107adantl 469 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
1097adantr 468 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
110 fvex 6431 . . . . . . . . . . . . . . 15 (𝐺𝑘) ∈ V
111 ifexg 4337 . . . . . . . . . . . . . . 15 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
112109, 110, 111sylancl 576 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
113 eqeq1 2821 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
114 fveq2 6418 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
115113, 114ifbieq2d 4315 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
116115, 9fvmptg 6511 . . . . . . . . . . . . . 14 ((𝑘𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
117108, 112, 116syl2anc 575 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
118 eldifn 3943 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
119118adantl 469 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
120 velsn 4397 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
121 elun2 3991 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
122120, 121sylbir 226 . . . . . . . . . . . . . . 15 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
123119, 122nsyl 137 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
124123iffalsed 4301 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
125 ssun1 3986 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
126 sscon 3954 . . . . . . . . . . . . . . . 16 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
127125, 126ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
128127sseli 3805 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
129 ssidd 3832 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
13027, 129, 3, 13suppssr 7571 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
131128, 130sylan2 582 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
132117, 124, 1313eqtrd 2855 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
13330, 132suppss 7570 . . . . . . . . . . 11 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
134133, 88sseldd 3810 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}))
135 elun 3963 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
136134, 135sylib 209 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
13796, 106, 136mpjaod 878 . . . . . . . 8 (𝜑 → ¬ 𝑋 ∈ (𝑂 dom 𝑂))
138 ioran 997 . . . . . . . 8 (¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)) ↔ (¬ (𝑂 dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
13981, 137, 138sylanbrc 574 . . . . . . 7 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
140 ordtri3 5986 . . . . . . . 8 ((Ord (𝑂 dom 𝑂) ∧ Ord 𝑋) → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
14191, 100, 140syl2anc 575 . . . . . . 7 (𝜑 → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
142139, 141mpbird 248 . . . . . 6 (𝜑 → (𝑂 dom 𝑂) = 𝑋)
143142oveq2d 6900 . . . . 5 (𝜑 → (𝐴𝑜 (𝑂 dom 𝑂)) = (𝐴𝑜 𝑋))
144142fveq2d 6422 . . . . . 6 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = (𝐹𝑋))
145144, 43eqtrd 2851 . . . . 5 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = 𝑌)
146143, 145oveq12d 6902 . . . 4 (𝜑 → ((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) = ((𝐴𝑜 𝑋) ·𝑜 𝑌))
147 nnord 7313 . . . . . . . . 9 ( dom 𝑂 ∈ ω → Ord dom 𝑂)
14820, 147syl 17 . . . . . . . 8 (𝜑 → Ord dom 𝑂)
149 sssucid 6028 . . . . . . . . . 10 dom 𝑂 ⊆ suc dom 𝑂
150149, 14syl5sseqr 3862 . . . . . . . . 9 (𝜑 dom 𝑂 ⊆ dom 𝑂)
151 f1ofo 6370 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂onto→(𝐹 supp ∅))
15237, 151syl 17 . . . . . . . . . . . 12 (𝜑𝑂:dom 𝑂onto→(𝐹 supp ∅))
153 foima 6346 . . . . . . . . . . . 12 (𝑂:dom 𝑂onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
154152, 153syl 17 . . . . . . . . . . 11 (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
155 ffn 6266 . . . . . . . . . . . . . 14 (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂)
15686, 155ax-mp 5 . . . . . . . . . . . . 13 𝑂 Fn dom 𝑂
157 fnsnfv 6489 . . . . . . . . . . . . 13 ((𝑂 Fn dom 𝑂 dom 𝑂 ∈ dom 𝑂) → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
158156, 69, 157sylancr 577 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
159142sneqd 4393 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = {𝑋})
160158, 159eqtr3d 2853 . . . . . . . . . . 11 (𝜑 → (𝑂 “ { dom 𝑂}) = {𝑋})
161154, 160difeq12d 3939 . . . . . . . . . 10 (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})) = ((𝐹 supp ∅) ∖ {𝑋}))
162 ordirr 5968 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → ¬ dom 𝑂 dom 𝑂)
163148, 162syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ dom 𝑂 dom 𝑂)
164 disjsn 4449 . . . . . . . . . . . . . . . 16 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ ¬ dom 𝑂 dom 𝑂)
165163, 164sylibr 225 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∩ { dom 𝑂}) = ∅)
166 disj3 4229 . . . . . . . . . . . . . . 15 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
167165, 166sylib 209 . . . . . . . . . . . . . 14 (𝜑 dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
168 difun2 4255 . . . . . . . . . . . . . 14 (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}) = ( dom 𝑂 ∖ { dom 𝑂})
169167, 168syl6eqr 2869 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
170 df-suc 5956 . . . . . . . . . . . . . . 15 suc dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂})
17114, 170syl6eq 2867 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂}))
172171difeq1d 3937 . . . . . . . . . . . . 13 (𝜑 → (dom 𝑂 ∖ { dom 𝑂}) = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
173169, 172eqtr4d 2854 . . . . . . . . . . . 12 (𝜑 dom 𝑂 = (dom 𝑂 ∖ { dom 𝑂}))
174173imaeq2d 5690 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) = (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})))
175 dff1o3 6369 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂onto→(𝐹 supp ∅) ∧ Fun 𝑂))
176175simprbi 486 . . . . . . . . . . . 12 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → Fun 𝑂)
177 imadif 6194 . . . . . . . . . . . 12 (Fun 𝑂 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
17837, 176, 1773syl 18 . . . . . . . . . . 11 (𝜑 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
179174, 178eqtrd 2851 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
1808, 102ssneldd 3812 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅))
181 disjsn 4449 . . . . . . . . . . . . 13 (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅))
182180, 181sylibr 225 . . . . . . . . . . . 12 (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅)
183 fvex 6431 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑋) ∈ V
184 dif1o 7827 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ ((𝐺𝑋) ∈ V ∧ (𝐺𝑋) ≠ ∅))
185183, 184mpbiran 691 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅)
18627ffnd 6267 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn 𝐵)
187 elsuppfn 7547 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
188186, 3, 52, 187syl3anc 1483 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
189185a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅))
190189bicomd 214 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐺𝑋) ≠ ∅ ↔ (𝐺𝑋) ∈ (V ∖ 1𝑜)))
191190anbi2d 616 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
192188, 191bitrd 270 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
1938sseld 3808 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋𝑋))
194192, 193sylbird 251 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜)) → 𝑋𝑋))
1956, 194mpand 678 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) → 𝑋𝑋))
196185, 195syl5bir 234 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑋) ≠ ∅ → 𝑋𝑋))
197196necon1bd 3007 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑋𝑋 → (𝐺𝑋) = ∅))
198102, 197mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑋) = ∅)
199198adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑋) = ∅)
200 fveqeq2 6427 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑋 → ((𝐺𝑘) = ∅ ↔ (𝐺𝑋) = ∅))
201199, 200syl5ibrcom 238 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺𝑘) = ∅))
202 eldifi 3942 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘𝐵)
203202adantl 469 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘𝐵)
2047adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌𝐴)
205204, 110, 111sylancl 576 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
206203, 205, 116syl2anc 575 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
207 ssidd 3832 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
20830, 207, 3, 13suppssr 7571 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = ∅)
209206, 208eqtr3d 2853 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅)
210 iffalse 4299 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
211210eqeq1d 2819 . . . . . . . . . . . . . . . 16 𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅ ↔ (𝐺𝑘) = ∅))
212209, 211syl5ibcom 236 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺𝑘) = ∅))
213201, 212pm2.61d 171 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑘) = ∅)
21427, 213suppss 7570 . . . . . . . . . . . . 13 (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅))
215 reldisj 4228 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
216214, 215syl 17 . . . . . . . . . . . 12 (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
217182, 216mpbid 223 . . . . . . . . . . 11 (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))
218 uncom 3967 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅))
219133, 218syl6sseq 3859 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)))
220 ssundif 4259 . . . . . . . . . . . 12 ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
221219, 220sylib 209 . . . . . . . . . . 11 (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
222217, 221eqssd 3826 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋}))
223161, 179, 2223eqtr4rd 2862 . . . . . . . . 9 (𝜑 → (𝐺 supp ∅) = (𝑂 dom 𝑂))
224 isores3 6819 . . . . . . . . 9 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 dom 𝑂)) → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
22535, 150, 223, 224syl3anc 1483 . . . . . . . 8 (𝜑 → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
226 cantnfp1.k . . . . . . . . . . 11 𝐾 = OrdIso( E , (𝐺 supp ∅))
2271, 2, 3, 226, 5cantnfcl 8821 . . . . . . . . . 10 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω))
228227simpld 484 . . . . . . . . 9 (𝜑 → E We (𝐺 supp ∅))
229 epse 5307 . . . . . . . . 9 E Se (𝐺 supp ∅)
230226oieu 8693 . . . . . . . . 9 (( E We (𝐺 supp ∅) ∧ E Se (𝐺 supp ∅)) → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
231228, 229, 230sylancl 576 . . . . . . . 8 (𝜑 → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
232148, 225, 231mpbi2and 694 . . . . . . 7 (𝜑 → ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾))
233232simpld 484 . . . . . 6 (𝜑 dom 𝑂 = dom 𝐾)
234233fveq2d 6422 . . . . 5 (𝜑 → (𝑀 dom 𝑂) = (𝑀‘dom 𝐾))
235 eleq1 2884 . . . . . . . . . 10 (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
236 fveq2 6418 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
237 fveq2 6418 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
238 cantnfp1.m . . . . . . . . . . . . . 14 𝑀 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐾𝑘)) ·𝑜 (𝐺‘(𝐾𝑘))) +𝑜 𝑧)), ∅)
239238seqom0g 7797 . . . . . . . . . . . . 13 (∅ ∈ V → (𝑀‘∅) = ∅)
24051, 239ax-mp 5 . . . . . . . . . . . 12 (𝑀‘∅) = ∅
241237, 240syl6eq 2867 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑀𝑥) = ∅)
242236, 241eqeq12d 2832 . . . . . . . . . 10 (𝑥 = ∅ → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘∅) = ∅))
243235, 242imbi12d 335 . . . . . . . . 9 (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)))
244243imbi2d 331 . . . . . . . 8 (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))))
245 eleq1 2884 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
246 fveq2 6418 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
247 fveq2 6418 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
248246, 247eqeq12d 2832 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻𝑦) = (𝑀𝑦)))
249245, 248imbi12d 335 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
250249imbi2d 331 . . . . . . . 8 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)))))
251 eleq1 2884 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂))
252 fveq2 6418 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
253 fveq2 6418 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑀𝑥) = (𝑀‘suc 𝑦))
254252, 253eqeq12d 2832 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
255251, 254imbi12d 335 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
256255imbi2d 331 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
257 eleq1 2884 . . . . . . . . . 10 (𝑥 = dom 𝑂 → (𝑥 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
258 fveq2 6418 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝐻𝑥) = (𝐻 dom 𝑂))
259 fveq2 6418 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝑀𝑥) = (𝑀 dom 𝑂))
260258, 259eqeq12d 2832 . . . . . . . . . 10 (𝑥 = dom 𝑂 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
261257, 260imbi12d 335 . . . . . . . . 9 (𝑥 = dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
262261imbi2d 331 . . . . . . . 8 (𝑥 = dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))))
26311seqom0g 7797 . . . . . . . . . 10 (∅ ∈ V → (𝐻‘∅) = ∅)
26451, 263mp1i 13 . . . . . . . . 9 (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)
265264a1i 11 . . . . . . . 8 (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))
266 nnord 7313 . . . . . . . . . . . . . . . 16 (dom 𝑂 ∈ ω → Ord dom 𝑂)
26717, 266syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Ord dom 𝑂)
268 ordtr 5964 . . . . . . . . . . . . . . 15 (Ord dom 𝑂 → Tr dom 𝑂)
269267, 268syl 17 . . . . . . . . . . . . . 14 (𝜑 → Tr dom 𝑂)
270 trsuc 6035 . . . . . . . . . . . . . 14 ((Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
271269, 270sylan 571 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
272271ex 399 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
273272imim1d 82 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
274 oveq2 6892 . . . . . . . . . . . . . 14 ((𝐻𝑦) = (𝑀𝑦) → (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
275 elnn 7315 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω)
276275ancoms 448 . . . . . . . . . . . . . . . . . 18 ((dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
27717, 276sylan 571 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
278271, 277syldan 581 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
2791, 2, 3, 4, 10, 11cantnfsuc 8824 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
280278, 279syldan 581 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
2811, 2, 3, 226, 5, 238cantnfsuc 8824 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
282278, 281syldan 581 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
283232simprd 485 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑂 dom 𝑂) = 𝐾)
284283fveq1d 6420 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
285284adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
28614eleq2d 2882 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
287286biimpa 464 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc dom 𝑂)
288148adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord dom 𝑂)
289 ordsucelsuc 7262 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord dom 𝑂 → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
290288, 289syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
291287, 290mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 dom 𝑂)
292 fvres 6437 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 dom 𝑂 → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
293291, 292syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
294285, 293eqtr3d 2853 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) = (𝑂𝑦))
295294oveq2d 6900 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴𝑜 (𝐾𝑦)) = (𝐴𝑜 (𝑂𝑦)))
296 suppssdm 7552 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
297296, 27fssdm 6282 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
298297adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵)
299233adantr 468 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → dom 𝑂 = dom 𝐾)
300291, 299eleqtrd 2898 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾)
301226oif 8684 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾:dom 𝐾⟶(𝐺 supp ∅)
302301ffvelrni 6590 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ dom 𝐾 → (𝐾𝑦) ∈ (𝐺 supp ∅))
303300, 302syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ (𝐺 supp ∅))
304298, 303sseldd 3810 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ 𝐵)
3057adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌𝐴)
306 fvex 6431 . . . . . . . . . . . . . . . . . . . . 21 (𝐺‘(𝐾𝑦)) ∈ V
307 ifexg 4337 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ (𝐺‘(𝐾𝑦)) ∈ V) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
308305, 306, 307sylancl 576 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
309 eqeq1 2821 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝑡 = 𝑋 ↔ (𝐾𝑦) = 𝑋))
310 fveq2 6418 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝐺𝑡) = (𝐺‘(𝐾𝑦)))
311309, 310ifbieq2d 4315 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
312311, 9fvmptg 6511 . . . . . . . . . . . . . . . . . . . 20 (((𝐾𝑦) ∈ 𝐵 ∧ if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
313304, 308, 312syl2anc 575 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
314294fveq2d 6422 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
315180adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅))
316 nelneq 2920 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾𝑦) = 𝑋)
317303, 315, 316syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾𝑦) = 𝑋)
318317iffalsed 4301 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) = (𝐺‘(𝐾𝑦)))
319313, 314, 3183eqtr3rd 2860 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
320295, 319oveq12d 6902 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) = ((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))))
321320oveq1d 6899 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
322282, 321eqtrd 2851 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
323280, 322eqeq12d 2832 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦))))
324274, 323syl5ibr 237 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
325324ex 399 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
326325a2d 29 . . . . . . . . . . 11 (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
327273, 326syld 47 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
328327a2i 14 . . . . . . . . 9 ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
329328a1i 11 . . . . . . . 8 (𝑦 ∈ ω → ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
330244, 250, 256, 262, 265, 329finds 7332 . . . . . . 7 ( dom 𝑂 ∈ ω → (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
33120, 330mpcom 38 . . . . . 6 (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
33269, 331mpd 15 . . . . 5 (𝜑 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))
3331, 2, 3, 226, 5, 238cantnfval 8822 . . . . 5 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾))
334234, 332, 3333eqtr4d 2861 . . . 4 (𝜑 → (𝐻 dom 𝑂) = ((𝐴 CNF 𝐵)‘𝐺))
335146, 334oveq12d 6902 . . 3 (𝜑 → (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
33622, 335eqtrd 2851 . 2 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
33712, 15, 3363eqtrd 2855 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2157  wne 2989  Vcvv 3402  cdif 3777  cun 3778  cin 3779  wss 3780  c0 4127  ifcif 4290  {csn 4381   cuni 4641   class class class wbr 4855  cmpt 4934  Tr wtr 4957   E cep 5236   Se wse 5281   We wwe 5282  ccnv 5323  dom cdm 5324  cres 5326  cima 5327  Ord word 5949  Oncon0 5950  suc csuc 5952  Fun wfun 6105   Fn wfn 6106  wf 6107  ontowfo 6109  1-1-ontowf1o 6110  cfv 6111   Isom wiso 6112  (class class class)co 6884  cmpt2 6886  ωcom 7305   supp csupp 7539  seq𝜔cseqom 7788  1𝑜c1o 7799   +𝑜 coa 7803   ·𝑜 comu 7804  𝑜 coe 7805   finSupp cfsupp 8524  OrdIsocoi 8663   CNF ccnf 8815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-seqom 7789  df-1o 7806  df-oadd 7810  df-er 7989  df-map 8104  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-oi 8664  df-cnf 8816
This theorem is referenced by:  cantnfp1  8835
  Copyright terms: Public domain W3C validator