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

Theorem cantnfp1lem3 8460
 Description: Lemma for cantnfp1 8461. (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 8458 . . 3 (𝜑𝐹𝑆)
11 cantnfp1.h . . 3 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐹‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
121, 2, 3, 4, 10, 11cantnfval 8448 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂))
13 cantnfp1.e . . . 4 (𝜑 → ∅ ∈ 𝑌)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 8459 . . 3 (𝜑 → dom 𝑂 = suc dom 𝑂)
1514fveq2d 6107 . 2 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
161, 2, 3, 4, 10cantnfcl 8447 . . . . . . 7 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω))
1716simprd 478 . . . . . 6 (𝜑 → dom 𝑂 ∈ ω)
1814, 17eqeltrrd 2689 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
19 peano2b 6973 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
2018, 19sylibr 223 . . . 4 (𝜑 dom 𝑂 ∈ ω)
211, 2, 3, 4, 10, 11cantnfsuc 8450 . . . 4 ((𝜑 dom 𝑂 ∈ ω) → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
2220, 21mpdan 699 . . 3 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
23 suppssdm 7195 . . . . . . . . . . . . . . . . 17 (𝐹 supp ∅) ⊆ dom 𝐹
247adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡𝐵) → 𝑌𝐴)
251, 2, 3cantnfs 8446 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
265, 25mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
2726simpld 474 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:𝐵𝐴)
2827ffvelrnda 6267 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
2924, 28ifcld 4081 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
3029, 9fmptd 6292 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝐵𝐴)
31 fdm 5964 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐵𝐴 → dom 𝐹 = 𝐵)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐵)
3323, 32syl5sseq 3616 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
343, 33ssexd 4733 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ∈ V)
3516simpld 474 . . . . . . . . . . . . . . 15 (𝜑 → E We (𝐹 supp ∅))
364oiiso 8325 . . . . . . . . . . . . . . 15 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
3734, 35, 36syl2anc 691 . . . . . . . . . . . . . 14 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
38 isof1o 6473 . . . . . . . . . . . . . 14 (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
40 f1ocnv 6062 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂)
41 f1of 6050 . . . . . . . . . . . . 13 (𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐹 supp ∅)⟶dom 𝑂)
4239, 40, 413syl 18 . . . . . . . . . . . 12 (𝜑𝑂:(𝐹 supp ∅)⟶dom 𝑂)
43 iftrue 4042 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = 𝑌)
4443, 9fvmptg 6189 . . . . . . . . . . . . . . 15 ((𝑋𝐵𝑌𝐴) → (𝐹𝑋) = 𝑌)
456, 7, 44syl2anc 691 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑋) = 𝑌)
46 onelon 5665 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
472, 7, 46syl2anc 691 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ On)
48 on0eln0 5697 . . . . . . . . . . . . . . . 16 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
4947, 48syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
5013, 49mpbid 221 . . . . . . . . . . . . . 14 (𝜑𝑌 ≠ ∅)
5145, 50eqnetrd 2849 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑋) ≠ ∅)
52 ffn 5958 . . . . . . . . . . . . . . 15 (𝐹:𝐵𝐴𝐹 Fn 𝐵)
5330, 52syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
54 0ex 4718 . . . . . . . . . . . . . . 15 ∅ ∈ V
5554a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
56 elsuppfn 7190 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
5753, 3, 55, 56syl3anc 1318 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
586, 51, 57mpbir2and 959 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐹 supp ∅))
5942, 58ffvelrnd 6268 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
60 elssuni 4403 . . . . . . . . . . 11 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
6159, 60syl 17 . . . . . . . . . 10 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
624oicl 8317 . . . . . . . . . . . 12 Ord dom 𝑂
63 ordelon 5664 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
6462, 59, 63sylancr 694 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
65 nnon 6963 . . . . . . . . . . . 12 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ On)
6620, 65syl 17 . . . . . . . . . . 11 (𝜑 dom 𝑂 ∈ On)
67 ontri1 5674 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ dom 𝑂 ∈ On) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6864, 66, 67syl2anc 691 . . . . . . . . . 10 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6961, 68mpbid 221 . . . . . . . . 9 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
70 sucidg 5720 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ suc dom 𝑂)
7120, 70syl 17 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
7271, 14eleqtrrd 2691 . . . . . . . . . . . 12 (𝜑 dom 𝑂 ∈ dom 𝑂)
73 isorel 6476 . . . . . . . . . . . 12 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
7437, 72, 59, 73syl12anc 1316 . . . . . . . . . . 11 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
75 fvex 6113 . . . . . . . . . . . 12 (𝑂𝑋) ∈ V
7675epelc 4951 . . . . . . . . . . 11 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
77 fvex 6113 . . . . . . . . . . . 12 (𝑂‘(𝑂𝑋)) ∈ V
7877epelc 4951 . . . . . . . . . . 11 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
7974, 76, 783bitr3g 301 . . . . . . . . . 10 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
80 f1ocnvfv2 6433 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
8139, 58, 80syl2anc 691 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
8281eleq2d 2673 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8379, 82bitrd 267 . . . . . . . . 9 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8469, 83mtbid 313 . . . . . . . 8 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
858sseld 3567 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → (𝑂 dom 𝑂) ∈ 𝑋))
86 onss 6882 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → 𝐵 ⊆ On)
873, 86syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ On)
8833, 87sstrd 3578 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) ⊆ On)
894oif 8318 . . . . . . . . . . . . . . . 16 𝑂:dom 𝑂⟶(𝐹 supp ∅)
9089ffvelrni 6266 . . . . . . . . . . . . . . 15 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
9172, 90syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
9288, 91sseldd 3569 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ On)
93 eloni 5650 . . . . . . . . . . . . 13 ((𝑂 dom 𝑂) ∈ On → Ord (𝑂 dom 𝑂))
9492, 93syl 17 . . . . . . . . . . . 12 (𝜑 → Ord (𝑂 dom 𝑂))
95 ordn2lp 5660 . . . . . . . . . . . 12 (Ord (𝑂 dom 𝑂) → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9694, 95syl 17 . . . . . . . . . . 11 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
97 imnan 437 . . . . . . . . . . 11 (((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)) ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9896, 97sylibr 223 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
9985, 98syld 46 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
100 onelon 5665 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
1013, 6, 100syl2anc 691 . . . . . . . . . . . 12 (𝜑𝑋 ∈ On)
102 eloni 5650 . . . . . . . . . . . 12 (𝑋 ∈ On → Ord 𝑋)
103101, 102syl 17 . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
104 ordirr 5658 . . . . . . . . . . 11 (Ord 𝑋 → ¬ 𝑋𝑋)
105103, 104syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑋𝑋)
106 elsni 4142 . . . . . . . . . . . 12 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑂 dom 𝑂) = 𝑋)
107106eleq2d 2673 . . . . . . . . . . 11 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂 dom 𝑂) ↔ 𝑋𝑋))
108107notbid 307 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂 dom 𝑂) ↔ ¬ 𝑋𝑋))
109105, 108syl5ibrcom 236 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
110 eldifi 3694 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
111110adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
1127adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
113 fvex 6113 . . . . . . . . . . . . . . 15 (𝐺𝑘) ∈ V
114 ifexg 4107 . . . . . . . . . . . . . . 15 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
115112, 113, 114sylancl 693 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
116 eqeq1 2614 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
117 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
118116, 117ifbieq2d 4061 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
119118, 9fvmptg 6189 . . . . . . . . . . . . . 14 ((𝑘𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
120111, 115, 119syl2anc 691 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
121 eldifn 3695 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
122121adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
123 velsn 4141 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
124 elun2 3743 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
125123, 124sylbir 224 . . . . . . . . . . . . . . 15 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
126122, 125nsyl 134 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
127126iffalsed 4047 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
128 ssun1 3738 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
129 sscon 3706 . . . . . . . . . . . . . . . 16 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
130128, 129ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
131130sseli 3564 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
132 ssid 3587 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
13427, 133, 3, 13suppssr 7213 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
135131, 134sylan2 490 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
136120, 127, 1353eqtrd 2648 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
13730, 136suppss 7212 . . . . . . . . . . 11 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
138137, 91sseldd 3569 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}))
139 elun 3715 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
140138, 139sylib 207 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
14199, 109, 140mpjaod 395 . . . . . . . 8 (𝜑 → ¬ 𝑋 ∈ (𝑂 dom 𝑂))
142 ioran 510 . . . . . . . 8 (¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)) ↔ (¬ (𝑂 dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
14384, 141, 142sylanbrc 695 . . . . . . 7 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
144 ordtri3 5676 . . . . . . . 8 ((Ord (𝑂 dom 𝑂) ∧ Ord 𝑋) → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
14594, 103, 144syl2anc 691 . . . . . . 7 (𝜑 → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
146143, 145mpbird 246 . . . . . 6 (𝜑 → (𝑂 dom 𝑂) = 𝑋)
147146oveq2d 6565 . . . . 5 (𝜑 → (𝐴𝑜 (𝑂 dom 𝑂)) = (𝐴𝑜 𝑋))
148146fveq2d 6107 . . . . . 6 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = (𝐹𝑋))
149148, 45eqtrd 2644 . . . . 5 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = 𝑌)
150147, 149oveq12d 6567 . . . 4 (𝜑 → ((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) = ((𝐴𝑜 𝑋) ·𝑜 𝑌))
151 nnord 6965 . . . . . . . . 9 ( dom 𝑂 ∈ ω → Ord dom 𝑂)
15220, 151syl 17 . . . . . . . 8 (𝜑 → Ord dom 𝑂)
153 sssucid 5719 . . . . . . . . . 10 dom 𝑂 ⊆ suc dom 𝑂
154153, 14syl5sseqr 3617 . . . . . . . . 9 (𝜑 dom 𝑂 ⊆ dom 𝑂)
155 f1ofo 6057 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂onto→(𝐹 supp ∅))
15639, 155syl 17 . . . . . . . . . . . 12 (𝜑𝑂:dom 𝑂onto→(𝐹 supp ∅))
157 foima 6033 . . . . . . . . . . . 12 (𝑂:dom 𝑂onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
158156, 157syl 17 . . . . . . . . . . 11 (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
159 ffn 5958 . . . . . . . . . . . . . 14 (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂)
16089, 159ax-mp 5 . . . . . . . . . . . . 13 𝑂 Fn dom 𝑂
161 fnsnfv 6168 . . . . . . . . . . . . 13 ((𝑂 Fn dom 𝑂 dom 𝑂 ∈ dom 𝑂) → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
162160, 72, 161sylancr 694 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
163146sneqd 4137 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = {𝑋})
164162, 163eqtr3d 2646 . . . . . . . . . . 11 (𝜑 → (𝑂 “ { dom 𝑂}) = {𝑋})
165158, 164difeq12d 3691 . . . . . . . . . 10 (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})) = ((𝐹 supp ∅) ∖ {𝑋}))
166 ordirr 5658 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → ¬ dom 𝑂 dom 𝑂)
167152, 166syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ dom 𝑂 dom 𝑂)
168 disjsn 4192 . . . . . . . . . . . . . . . 16 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ ¬ dom 𝑂 dom 𝑂)
169167, 168sylibr 223 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∩ { dom 𝑂}) = ∅)
170 disj3 3973 . . . . . . . . . . . . . . 15 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
171169, 170sylib 207 . . . . . . . . . . . . . 14 (𝜑 dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
172 difun2 4000 . . . . . . . . . . . . . 14 (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}) = ( dom 𝑂 ∖ { dom 𝑂})
173171, 172syl6eqr 2662 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
174 df-suc 5646 . . . . . . . . . . . . . . 15 suc dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂})
17514, 174syl6eq 2660 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂}))
176175difeq1d 3689 . . . . . . . . . . . . 13 (𝜑 → (dom 𝑂 ∖ { dom 𝑂}) = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
177173, 176eqtr4d 2647 . . . . . . . . . . . 12 (𝜑 dom 𝑂 = (dom 𝑂 ∖ { dom 𝑂}))
178177imaeq2d 5385 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) = (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})))
179 dff1o3 6056 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂onto→(𝐹 supp ∅) ∧ Fun 𝑂))
180179simprbi 479 . . . . . . . . . . . 12 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → Fun 𝑂)
181 imadif 5887 . . . . . . . . . . . 12 (Fun 𝑂 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
18239, 180, 1813syl 18 . . . . . . . . . . 11 (𝜑 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
183178, 182eqtrd 2644 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
1848, 105ssneldd 3571 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅))
185 disjsn 4192 . . . . . . . . . . . . 13 (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅))
186184, 185sylibr 223 . . . . . . . . . . . 12 (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅)
187 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑋) ∈ V
188 dif1o 7467 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ ((𝐺𝑋) ∈ V ∧ (𝐺𝑋) ≠ ∅))
189187, 188mpbiran 955 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅)
190 ffn 5958 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺:𝐵𝐴𝐺 Fn 𝐵)
19127, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn 𝐵)
192 elsuppfn 7190 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
193191, 3, 55, 192syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
194189a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅))
195194bicomd 212 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐺𝑋) ≠ ∅ ↔ (𝐺𝑋) ∈ (V ∖ 1𝑜)))
196195anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
197193, 196bitrd 267 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
1988sseld 3567 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋𝑋))
199197, 198sylbird 249 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜)) → 𝑋𝑋))
2006, 199mpand 707 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) → 𝑋𝑋))
201189, 200syl5bir 232 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑋) ≠ ∅ → 𝑋𝑋))
202201necon1bd 2800 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑋𝑋 → (𝐺𝑋) = ∅))
203105, 202mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑋) = ∅)
204203adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑋) = ∅)
205 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑋 → (𝐺𝑘) = (𝐺𝑋))
206205eqeq1d 2612 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑋 → ((𝐺𝑘) = ∅ ↔ (𝐺𝑋) = ∅))
207204, 206syl5ibrcom 236 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺𝑘) = ∅))
208 eldifi 3694 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘𝐵)
209208adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘𝐵)
2107adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌𝐴)
211210, 113, 114sylancl 693 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
212209, 211, 119syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
213 ssid 3587 . . . . . . . . . . . . . . . . . . 19 (𝐹 supp ∅) ⊆ (𝐹 supp ∅)
214213a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
21530, 214, 3, 13suppssr 7213 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = ∅)
216212, 215eqtr3d 2646 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅)
217 iffalse 4045 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
218217eqeq1d 2612 . . . . . . . . . . . . . . . 16 𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅ ↔ (𝐺𝑘) = ∅))
219216, 218syl5ibcom 234 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺𝑘) = ∅))
220207, 219pm2.61d 169 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑘) = ∅)
22127, 220suppss 7212 . . . . . . . . . . . . 13 (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅))
222 reldisj 3972 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
223221, 222syl 17 . . . . . . . . . . . 12 (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
224186, 223mpbid 221 . . . . . . . . . . 11 (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))
225 uncom 3719 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅))
226137, 225syl6sseq 3614 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)))
227 ssundif 4004 . . . . . . . . . . . 12 ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
228226, 227sylib 207 . . . . . . . . . . 11 (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
229224, 228eqssd 3585 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋}))
230165, 183, 2293eqtr4rd 2655 . . . . . . . . 9 (𝜑 → (𝐺 supp ∅) = (𝑂 dom 𝑂))
231 isores3 6485 . . . . . . . . 9 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 dom 𝑂)) → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
23237, 154, 230, 231syl3anc 1318 . . . . . . . 8 (𝜑 → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
233 cantnfp1.k . . . . . . . . . . 11 𝐾 = OrdIso( E , (𝐺 supp ∅))
2341, 2, 3, 233, 5cantnfcl 8447 . . . . . . . . . 10 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω))
235234simpld 474 . . . . . . . . 9 (𝜑 → E We (𝐺 supp ∅))
236 epse 5021 . . . . . . . . 9 E Se (𝐺 supp ∅)
237233oieu 8327 . . . . . . . . 9 (( E We (𝐺 supp ∅) ∧ E Se (𝐺 supp ∅)) → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
238235, 236, 237sylancl 693 . . . . . . . 8 (𝜑 → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
239152, 232, 238mpbi2and 958 . . . . . . 7 (𝜑 → ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾))
240239simpld 474 . . . . . 6 (𝜑 dom 𝑂 = dom 𝐾)
241240fveq2d 6107 . . . . 5 (𝜑 → (𝑀 dom 𝑂) = (𝑀‘dom 𝐾))
242 eleq1 2676 . . . . . . . . . 10 (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
243 fveq2 6103 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
244 fveq2 6103 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
245 cantnfp1.m . . . . . . . . . . . . . 14 𝑀 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐾𝑘)) ·𝑜 (𝐺‘(𝐾𝑘))) +𝑜 𝑧)), ∅)
246245seqom0g 7438 . . . . . . . . . . . . 13 (∅ ∈ V → (𝑀‘∅) = ∅)
24754, 246ax-mp 5 . . . . . . . . . . . 12 (𝑀‘∅) = ∅
248244, 247syl6eq 2660 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑀𝑥) = ∅)
249243, 248eqeq12d 2625 . . . . . . . . . 10 (𝑥 = ∅ → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘∅) = ∅))
250242, 249imbi12d 333 . . . . . . . . 9 (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)))
251250imbi2d 329 . . . . . . . 8 (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))))
252 eleq1 2676 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
253 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
254 fveq2 6103 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
255253, 254eqeq12d 2625 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻𝑦) = (𝑀𝑦)))
256252, 255imbi12d 333 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
257256imbi2d 329 . . . . . . . 8 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)))))
258 eleq1 2676 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂))
259 fveq2 6103 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
260 fveq2 6103 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑀𝑥) = (𝑀‘suc 𝑦))
261259, 260eqeq12d 2625 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
262258, 261imbi12d 333 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
263262imbi2d 329 . . . . . . . 8 (𝑥 = suc 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
264 eleq1 2676 . . . . . . . . . 10 (𝑥 = dom 𝑂 → (𝑥 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
265 fveq2 6103 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝐻𝑥) = (𝐻 dom 𝑂))
266 fveq2 6103 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝑀𝑥) = (𝑀 dom 𝑂))
267265, 266eqeq12d 2625 . . . . . . . . . 10 (𝑥 = dom 𝑂 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
268264, 267imbi12d 333 . . . . . . . . 9 (𝑥 = dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
269268imbi2d 329 . . . . . . . 8 (𝑥 = dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))))
27011seqom0g 7438 . . . . . . . . . 10 (∅ ∈ V → (𝐻‘∅) = ∅)
27154, 270mp1i 13 . . . . . . . . 9 (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)
272271a1i 11 . . . . . . . 8 (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))
273 nnord 6965 . . . . . . . . . . . . . . . 16 (dom 𝑂 ∈ ω → Ord dom 𝑂)
27417, 273syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Ord dom 𝑂)
275 ordtr 5654 . . . . . . . . . . . . . . 15 (Ord dom 𝑂 → Tr dom 𝑂)
276274, 275syl 17 . . . . . . . . . . . . . 14 (𝜑 → Tr dom 𝑂)
277 trsuc 5727 . . . . . . . . . . . . . 14 ((Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
278276, 277sylan 487 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
279278ex 449 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
280279imim1d 80 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
281 oveq2 6557 . . . . . . . . . . . . . 14 ((𝐻𝑦) = (𝑀𝑦) → (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
282 elnn 6967 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω)
283282ancoms 468 . . . . . . . . . . . . . . . . . 18 ((dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
28417, 283sylan 487 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
285278, 284syldan 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
2861, 2, 3, 4, 10, 11cantnfsuc 8450 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
287285, 286syldan 486 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
2881, 2, 3, 233, 5, 245cantnfsuc 8450 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
289285, 288syldan 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
290239simprd 478 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑂 dom 𝑂) = 𝐾)
291290fveq1d 6105 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
292291adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
29314eleq2d 2673 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
294293biimpa 500 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc dom 𝑂)
295152adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord dom 𝑂)
296 ordsucelsuc 6914 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord dom 𝑂 → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
297295, 296syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
298294, 297mpbird 246 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 dom 𝑂)
299 fvres 6117 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 dom 𝑂 → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
300298, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
301292, 300eqtr3d 2646 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) = (𝑂𝑦))
302301oveq2d 6565 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴𝑜 (𝐾𝑦)) = (𝐴𝑜 (𝑂𝑦)))
303 suppssdm 7195 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
304 fdm 5964 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
30527, 304syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = 𝐵)
306303, 305syl5sseq 3616 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
307306adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵)
308240adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → dom 𝑂 = dom 𝐾)
309298, 308eleqtrd 2690 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾)
310233oif 8318 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾:dom 𝐾⟶(𝐺 supp ∅)
311310ffvelrni 6266 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ dom 𝐾 → (𝐾𝑦) ∈ (𝐺 supp ∅))
312309, 311syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ (𝐺 supp ∅))
313307, 312sseldd 3569 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ 𝐵)
3147adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌𝐴)
315 fvex 6113 . . . . . . . . . . . . . . . . . . . . 21 (𝐺‘(𝐾𝑦)) ∈ V
316 ifexg 4107 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ (𝐺‘(𝐾𝑦)) ∈ V) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
317314, 315, 316sylancl 693 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
318 eqeq1 2614 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝑡 = 𝑋 ↔ (𝐾𝑦) = 𝑋))
319 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝐺𝑡) = (𝐺‘(𝐾𝑦)))
320318, 319ifbieq2d 4061 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
321320, 9fvmptg 6189 . . . . . . . . . . . . . . . . . . . 20 (((𝐾𝑦) ∈ 𝐵 ∧ if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
322313, 317, 321syl2anc 691 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
323301fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
324184adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅))
325 nelneq 2712 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾𝑦) = 𝑋)
326312, 324, 325syl2anc 691 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾𝑦) = 𝑋)
327326iffalsed 4047 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) = (𝐺‘(𝐾𝑦)))
328322, 323, 3273eqtr3rd 2653 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
329302, 328oveq12d 6567 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) = ((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))))
330329oveq1d 6564 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
331289, 330eqtrd 2644 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
332287, 331eqeq12d 2625 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦))))
333281, 332syl5ibr 235 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
334333ex 449 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
335334a2d 29 . . . . . . . . . . 11 (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
336280, 335syld 46 . . . . . . . . . 10 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
337336a2i 14 . . . . . . . . 9 ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
338337a1i 11 . . . . . . . 8 (𝑦 ∈ ω → ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))))
339251, 257, 263, 269, 272, 338finds 6984 . . . . . . 7 ( dom 𝑂 ∈ ω → (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
34020, 339mpcom 37 . . . . . 6 (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
34172, 340mpd 15 . . . . 5 (𝜑 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))
3421, 2, 3, 233, 5, 245cantnfval 8448 . . . . 5 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾))
343241, 341, 3423eqtr4d 2654 . . . 4 (𝜑 → (𝐻 dom 𝑂) = ((𝐴 CNF 𝐵)‘𝐺))
344150, 343oveq12d 6567 . . 3 (𝜑 → (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
34522, 344eqtrd 2644 . 2 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
34612, 15, 3453eqtrd 2648 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  {csn 4125  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643  Tr wtr 4680   E cep 4947   Se wse 4995   We wwe 4996  ◡ccnv 5037  dom cdm 5038   ↾ cres 5040   “ cima 5041  Ord word 5639  Oncon0 5640  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957   supp csupp 7182  seq𝜔cseqom 7429  1𝑜c1o 7440   +𝑜 coa 7444   ·𝑜 comu 7445   ↑𝑜 coe 7446   finSupp cfsupp 8158  OrdIsocoi 8297   CNF ccnf 8441 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seqom 7430  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-cnf 8442 This theorem is referenced by:  cantnfp1  8461
 Copyright terms: Public domain W3C validator