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

Theorem cantnfp1lem3 8752
Description: Lemma for cantnfp1 8753. (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 8750 . . 3 (𝜑𝐹𝑆)
11 cantnfp1.h . . 3 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝑂𝑘)) ·𝑜 (𝐹‘(𝑂𝑘))) +𝑜 𝑧)), ∅)
121, 2, 3, 4, 10, 11cantnfval 8740 . 2 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂))
13 cantnfp1.e . . . 4 (𝜑 → ∅ ∈ 𝑌)
141, 2, 3, 5, 6, 7, 8, 9, 13, 4cantnfp1lem2 8751 . . 3 (𝜑 → dom 𝑂 = suc dom 𝑂)
1514fveq2d 6357 . 2 (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc dom 𝑂))
161, 2, 3, 4, 10cantnfcl 8739 . . . . . . 7 (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω))
1716simprd 482 . . . . . 6 (𝜑 → dom 𝑂 ∈ ω)
1814, 17eqeltrrd 2840 . . . . 5 (𝜑 → suc dom 𝑂 ∈ ω)
19 peano2b 7247 . . . . 5 ( dom 𝑂 ∈ ω ↔ suc dom 𝑂 ∈ ω)
2018, 19sylibr 224 . . . 4 (𝜑 dom 𝑂 ∈ ω)
211, 2, 3, 4, 10, 11cantnfsuc 8742 . . . 4 ((𝜑 dom 𝑂 ∈ ω) → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
2220, 21mpdan 705 . . 3 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)))
23 suppssdm 7477 . . . . . . . . . . . . . . . . 17 (𝐹 supp ∅) ⊆ dom 𝐹
247adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡𝐵) → 𝑌𝐴)
251, 2, 3cantnfs 8738 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐺𝑆 ↔ (𝐺:𝐵𝐴𝐺 finSupp ∅)))
265, 25mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺:𝐵𝐴𝐺 finSupp ∅))
2726simpld 477 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐺:𝐵𝐴)
2827ffvelrnda 6523 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑡𝐵) → (𝐺𝑡) ∈ 𝐴)
2924, 28ifcld 4275 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑡𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) ∈ 𝐴)
3029, 9fmptd 6549 . . . . . . . . . . . . . . . . . 18 (𝜑𝐹:𝐵𝐴)
31 fdm 6212 . . . . . . . . . . . . . . . . . 18 (𝐹:𝐵𝐴 → dom 𝐹 = 𝐵)
3230, 31syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom 𝐹 = 𝐵)
3323, 32syl5sseq 3794 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹 supp ∅) ⊆ 𝐵)
343, 33ssexd 4957 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹 supp ∅) ∈ V)
3516simpld 477 . . . . . . . . . . . . . . 15 (𝜑 → E We (𝐹 supp ∅))
364oiiso 8609 . . . . . . . . . . . . . . 15 (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
3734, 35, 36syl2anc 696 . . . . . . . . . . . . . 14 (𝜑𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)))
38 isof1o 6737 . . . . . . . . . . . . . 14 (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
3937, 38syl 17 . . . . . . . . . . . . 13 (𝜑𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅))
40 f1ocnv 6311 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂)
41 f1of 6299 . . . . . . . . . . . . 13 (𝑂:(𝐹 supp ∅)–1-1-onto→dom 𝑂𝑂:(𝐹 supp ∅)⟶dom 𝑂)
4239, 40, 413syl 18 . . . . . . . . . . . 12 (𝜑𝑂:(𝐹 supp ∅)⟶dom 𝑂)
43 iftrue 4236 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = 𝑌)
4443, 9fvmptg 6443 . . . . . . . . . . . . . . 15 ((𝑋𝐵𝑌𝐴) → (𝐹𝑋) = 𝑌)
456, 7, 44syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝑋) = 𝑌)
46 onelon 5909 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ On ∧ 𝑌𝐴) → 𝑌 ∈ On)
472, 7, 46syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ On)
48 on0eln0 5941 . . . . . . . . . . . . . . . 16 (𝑌 ∈ On → (∅ ∈ 𝑌𝑌 ≠ ∅))
4947, 48syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (∅ ∈ 𝑌𝑌 ≠ ∅))
5013, 49mpbid 222 . . . . . . . . . . . . . 14 (𝜑𝑌 ≠ ∅)
5145, 50eqnetrd 2999 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑋) ≠ ∅)
52 ffn 6206 . . . . . . . . . . . . . . 15 (𝐹:𝐵𝐴𝐹 Fn 𝐵)
5330, 52syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
54 0ex 4942 . . . . . . . . . . . . . . 15 ∅ ∈ V
5554a1i 11 . . . . . . . . . . . . . 14 (𝜑 → ∅ ∈ V)
56 elsuppfn 7472 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
5753, 3, 55, 56syl3anc 1477 . . . . . . . . . . . . 13 (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋𝐵 ∧ (𝐹𝑋) ≠ ∅)))
586, 51, 57mpbir2and 995 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝐹 supp ∅))
5942, 58ffvelrnd 6524 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ dom 𝑂)
60 elssuni 4619 . . . . . . . . . . 11 ((𝑂𝑋) ∈ dom 𝑂 → (𝑂𝑋) ⊆ dom 𝑂)
6159, 60syl 17 . . . . . . . . . 10 (𝜑 → (𝑂𝑋) ⊆ dom 𝑂)
624oicl 8601 . . . . . . . . . . . 12 Ord dom 𝑂
63 ordelon 5908 . . . . . . . . . . . 12 ((Ord dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂) → (𝑂𝑋) ∈ On)
6462, 59, 63sylancr 698 . . . . . . . . . . 11 (𝜑 → (𝑂𝑋) ∈ On)
65 nnon 7237 . . . . . . . . . . . 12 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ On)
6620, 65syl 17 . . . . . . . . . . 11 (𝜑 dom 𝑂 ∈ On)
67 ontri1 5918 . . . . . . . . . . 11 (((𝑂𝑋) ∈ On ∧ dom 𝑂 ∈ On) → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6864, 66, 67syl2anc 696 . . . . . . . . . 10 (𝜑 → ((𝑂𝑋) ⊆ dom 𝑂 ↔ ¬ dom 𝑂 ∈ (𝑂𝑋)))
6961, 68mpbid 222 . . . . . . . . 9 (𝜑 → ¬ dom 𝑂 ∈ (𝑂𝑋))
70 sucidg 5964 . . . . . . . . . . . . . 14 ( dom 𝑂 ∈ ω → dom 𝑂 ∈ suc dom 𝑂)
7120, 70syl 17 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 ∈ suc dom 𝑂)
7271, 14eleqtrrd 2842 . . . . . . . . . . . 12 (𝜑 dom 𝑂 ∈ dom 𝑂)
73 isorel 6740 . . . . . . . . . . . 12 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ( dom 𝑂 ∈ dom 𝑂 ∧ (𝑂𝑋) ∈ dom 𝑂)) → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
7437, 72, 59, 73syl12anc 1475 . . . . . . . . . . 11 (𝜑 → ( dom 𝑂 E (𝑂𝑋) ↔ (𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋))))
75 fvex 6363 . . . . . . . . . . . 12 (𝑂𝑋) ∈ V
7675epelc 5181 . . . . . . . . . . 11 ( dom 𝑂 E (𝑂𝑋) ↔ dom 𝑂 ∈ (𝑂𝑋))
77 fvex 6363 . . . . . . . . . . . 12 (𝑂‘(𝑂𝑋)) ∈ V
7877epelc 5181 . . . . . . . . . . 11 ((𝑂 dom 𝑂) E (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)))
7974, 76, 783bitr3g 302 . . . . . . . . . 10 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋))))
80 f1ocnvfv2 6697 . . . . . . . . . . . 12 ((𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(𝑂𝑋)) = 𝑋)
8139, 58, 80syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝑂‘(𝑂𝑋)) = 𝑋)
8281eleq2d 2825 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝑂‘(𝑂𝑋)) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8379, 82bitrd 268 . . . . . . . . 9 (𝜑 → ( dom 𝑂 ∈ (𝑂𝑋) ↔ (𝑂 dom 𝑂) ∈ 𝑋))
8469, 83mtbid 313 . . . . . . . 8 (𝜑 → ¬ (𝑂 dom 𝑂) ∈ 𝑋)
858sseld 3743 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → (𝑂 dom 𝑂) ∈ 𝑋))
86 onss 7156 . . . . . . . . . . . . . . . 16 (𝐵 ∈ On → 𝐵 ⊆ On)
873, 86syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ On)
8833, 87sstrd 3754 . . . . . . . . . . . . . 14 (𝜑 → (𝐹 supp ∅) ⊆ On)
894oif 8602 . . . . . . . . . . . . . . . 16 𝑂:dom 𝑂⟶(𝐹 supp ∅)
9089ffvelrni 6522 . . . . . . . . . . . . . . 15 ( dom 𝑂 ∈ dom 𝑂 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
9172, 90syl 17 . . . . . . . . . . . . . 14 (𝜑 → (𝑂 dom 𝑂) ∈ (𝐹 supp ∅))
9288, 91sseldd 3745 . . . . . . . . . . . . 13 (𝜑 → (𝑂 dom 𝑂) ∈ On)
93 eloni 5894 . . . . . . . . . . . . 13 ((𝑂 dom 𝑂) ∈ On → Ord (𝑂 dom 𝑂))
9492, 93syl 17 . . . . . . . . . . . 12 (𝜑 → Ord (𝑂 dom 𝑂))
95 ordn2lp 5904 . . . . . . . . . . . 12 (Ord (𝑂 dom 𝑂) → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9694, 95syl 17 . . . . . . . . . . 11 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
97 imnan 437 . . . . . . . . . . 11 (((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)) ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
9896, 97sylibr 224 . . . . . . . . . 10 (𝜑 → ((𝑂 dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
9985, 98syld 47 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
100 onelon 5909 . . . . . . . . . . . . 13 ((𝐵 ∈ On ∧ 𝑋𝐵) → 𝑋 ∈ On)
1013, 6, 100syl2anc 696 . . . . . . . . . . . 12 (𝜑𝑋 ∈ On)
102 eloni 5894 . . . . . . . . . . . 12 (𝑋 ∈ On → Ord 𝑋)
103101, 102syl 17 . . . . . . . . . . 11 (𝜑 → Ord 𝑋)
104 ordirr 5902 . . . . . . . . . . 11 (Ord 𝑋 → ¬ 𝑋𝑋)
105103, 104syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑋𝑋)
106 elsni 4338 . . . . . . . . . . . 12 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑂 dom 𝑂) = 𝑋)
107106eleq2d 2825 . . . . . . . . . . 11 ((𝑂 dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂 dom 𝑂) ↔ 𝑋𝑋))
108107notbid 307 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂 dom 𝑂) ↔ ¬ 𝑋𝑋))
109105, 108syl5ibrcom 237 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
110 eldifi 3875 . . . . . . . . . . . . . . 15 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘𝐵)
111110adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘𝐵)
1127adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌𝐴)
113 fvex 6363 . . . . . . . . . . . . . . 15 (𝐺𝑘) ∈ V
114 ifexg 4301 . . . . . . . . . . . . . . 15 ((𝑌𝐴 ∧ (𝐺𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
115112, 113, 114sylancl 697 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
116 eqeq1 2764 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝑡 = 𝑋𝑘 = 𝑋))
117 fveq2 6353 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑘 → (𝐺𝑡) = (𝐺𝑘))
118116, 117ifbieq2d 4255 . . . . . . . . . . . . . . 15 (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
119118, 9fvmptg 6443 . . . . . . . . . . . . . 14 ((𝑘𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
120111, 115, 119syl2anc 696 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
121 eldifn 3876 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
122121adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
123 velsn 4337 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋)
124 elun2 3924 . . . . . . . . . . . . . . . 16 (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
125123, 124sylbir 225 . . . . . . . . . . . . . . 15 (𝑘 = 𝑋𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋}))
126122, 125nsyl 135 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋)
127126iffalsed 4241 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
128 ssun1 3919 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})
129 sscon 3887 . . . . . . . . . . . . . . . 16 ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)))
130128, 129ax-mp 5 . . . . . . . . . . . . . . 15 (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))
131130sseli 3740 . . . . . . . . . . . . . 14 (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅)))
132 ssid 3765 . . . . . . . . . . . . . . . 16 (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
133132a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
13427, 133, 3, 13suppssr 7496 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺𝑘) = ∅)
135131, 134sylan2 492 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺𝑘) = ∅)
136120, 127, 1353eqtrd 2798 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹𝑘) = ∅)
13730, 136suppss 7495 . . . . . . . . . . 11 (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}))
138137, 91sseldd 3745 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}))
139 elun 3896 . . . . . . . . . 10 ((𝑂 dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
140138, 139sylib 208 . . . . . . . . 9 (𝜑 → ((𝑂 dom 𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂 dom 𝑂) ∈ {𝑋}))
14199, 109, 140mpjaod 395 . . . . . . . 8 (𝜑 → ¬ 𝑋 ∈ (𝑂 dom 𝑂))
142 ioran 512 . . . . . . . 8 (¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)) ↔ (¬ (𝑂 dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂 dom 𝑂)))
14384, 141, 142sylanbrc 701 . . . . . . 7 (𝜑 → ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂)))
144 ordtri3 5920 . . . . . . . 8 ((Ord (𝑂 dom 𝑂) ∧ Ord 𝑋) → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
14594, 103, 144syl2anc 696 . . . . . . 7 (𝜑 → ((𝑂 dom 𝑂) = 𝑋 ↔ ¬ ((𝑂 dom 𝑂) ∈ 𝑋𝑋 ∈ (𝑂 dom 𝑂))))
146143, 145mpbird 247 . . . . . 6 (𝜑 → (𝑂 dom 𝑂) = 𝑋)
147146oveq2d 6830 . . . . 5 (𝜑 → (𝐴𝑜 (𝑂 dom 𝑂)) = (𝐴𝑜 𝑋))
148146fveq2d 6357 . . . . . 6 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = (𝐹𝑋))
149148, 45eqtrd 2794 . . . . 5 (𝜑 → (𝐹‘(𝑂 dom 𝑂)) = 𝑌)
150147, 149oveq12d 6832 . . . 4 (𝜑 → ((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) = ((𝐴𝑜 𝑋) ·𝑜 𝑌))
151 nnord 7239 . . . . . . . . 9 ( dom 𝑂 ∈ ω → Ord dom 𝑂)
15220, 151syl 17 . . . . . . . 8 (𝜑 → Ord dom 𝑂)
153 sssucid 5963 . . . . . . . . . 10 dom 𝑂 ⊆ suc dom 𝑂
154153, 14syl5sseqr 3795 . . . . . . . . 9 (𝜑 dom 𝑂 ⊆ dom 𝑂)
155 f1ofo 6306 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂onto→(𝐹 supp ∅))
15639, 155syl 17 . . . . . . . . . . . 12 (𝜑𝑂:dom 𝑂onto→(𝐹 supp ∅))
157 foima 6282 . . . . . . . . . . . 12 (𝑂:dom 𝑂onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
158156, 157syl 17 . . . . . . . . . . 11 (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅))
159 ffn 6206 . . . . . . . . . . . . . 14 (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂)
16089, 159ax-mp 5 . . . . . . . . . . . . 13 𝑂 Fn dom 𝑂
161 fnsnfv 6421 . . . . . . . . . . . . 13 ((𝑂 Fn dom 𝑂 dom 𝑂 ∈ dom 𝑂) → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
162160, 72, 161sylancr 698 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = (𝑂 “ { dom 𝑂}))
163146sneqd 4333 . . . . . . . . . . . 12 (𝜑 → {(𝑂 dom 𝑂)} = {𝑋})
164162, 163eqtr3d 2796 . . . . . . . . . . 11 (𝜑 → (𝑂 “ { dom 𝑂}) = {𝑋})
165158, 164difeq12d 3872 . . . . . . . . . 10 (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})) = ((𝐹 supp ∅) ∖ {𝑋}))
166 ordirr 5902 . . . . . . . . . . . . . . . . 17 (Ord dom 𝑂 → ¬ dom 𝑂 dom 𝑂)
167152, 166syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ dom 𝑂 dom 𝑂)
168 disjsn 4390 . . . . . . . . . . . . . . . 16 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ ¬ dom 𝑂 dom 𝑂)
169167, 168sylibr 224 . . . . . . . . . . . . . . 15 (𝜑 → ( dom 𝑂 ∩ { dom 𝑂}) = ∅)
170 disj3 4164 . . . . . . . . . . . . . . 15 (( dom 𝑂 ∩ { dom 𝑂}) = ∅ ↔ dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
171169, 170sylib 208 . . . . . . . . . . . . . 14 (𝜑 dom 𝑂 = ( dom 𝑂 ∖ { dom 𝑂}))
172 difun2 4192 . . . . . . . . . . . . . 14 (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}) = ( dom 𝑂 ∖ { dom 𝑂})
173171, 172syl6eqr 2812 . . . . . . . . . . . . 13 (𝜑 dom 𝑂 = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
174 df-suc 5890 . . . . . . . . . . . . . . 15 suc dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂})
17514, 174syl6eq 2810 . . . . . . . . . . . . . 14 (𝜑 → dom 𝑂 = ( dom 𝑂 ∪ { dom 𝑂}))
176175difeq1d 3870 . . . . . . . . . . . . 13 (𝜑 → (dom 𝑂 ∖ { dom 𝑂}) = (( dom 𝑂 ∪ { dom 𝑂}) ∖ { dom 𝑂}))
177173, 176eqtr4d 2797 . . . . . . . . . . . 12 (𝜑 dom 𝑂 = (dom 𝑂 ∖ { dom 𝑂}))
178177imaeq2d 5624 . . . . . . . . . . 11 (𝜑 → (𝑂 dom 𝑂) = (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})))
179 dff1o3 6305 . . . . . . . . . . . . 13 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂onto→(𝐹 supp ∅) ∧ Fun 𝑂))
180179simprbi 483 . . . . . . . . . . . 12 (𝑂:dom 𝑂1-1-onto→(𝐹 supp ∅) → Fun 𝑂)
181 imadif 6134 . . . . . . . . . . . 12 (Fun 𝑂 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
18239, 180, 1813syl 18 . . . . . . . . . . 11 (𝜑 → (𝑂 “ (dom 𝑂 ∖ { dom 𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
183178, 182eqtrd 2794 . . . . . . . . . 10 (𝜑 → (𝑂 dom 𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ { dom 𝑂})))
1848, 105ssneldd 3747 . . . . . . . . . . . . 13 (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅))
185 disjsn 4390 . . . . . . . . . . . . 13 (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅))
186184, 185sylibr 224 . . . . . . . . . . . 12 (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅)
187 fvex 6363 . . . . . . . . . . . . . . . . . . . . 21 (𝐺𝑋) ∈ V
188 dif1o 7751 . . . . . . . . . . . . . . . . . . . . 21 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ ((𝐺𝑋) ∈ V ∧ (𝐺𝑋) ≠ ∅))
189187, 188mpbiran 991 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅)
190 ffn 6206 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐺:𝐵𝐴𝐺 Fn 𝐵)
19127, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝐺 Fn 𝐵)
192 elsuppfn 7472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐺 Fn 𝐵𝐵 ∈ On ∧ ∅ ∈ V) → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
193191, 3, 55, 192syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅)))
194189a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) ↔ (𝐺𝑋) ≠ ∅))
195194bicomd 213 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝐺𝑋) ≠ ∅ ↔ (𝐺𝑋) ∈ (V ∖ 1𝑜)))
196195anbi2d 742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ≠ ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
197193, 196bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜))))
1988sseld 3743 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋𝑋))
199197, 198sylbird 250 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑋𝐵 ∧ (𝐺𝑋) ∈ (V ∖ 1𝑜)) → 𝑋𝑋))
2006, 199mpand 713 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝑋) ∈ (V ∖ 1𝑜) → 𝑋𝑋))
201189, 200syl5bir 233 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐺𝑋) ≠ ∅ → 𝑋𝑋))
202201necon1bd 2950 . . . . . . . . . . . . . . . . . 18 (𝜑 → (¬ 𝑋𝑋 → (𝐺𝑋) = ∅))
203105, 202mpd 15 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐺𝑋) = ∅)
204203adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑋) = ∅)
205 fveq2 6353 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑋 → (𝐺𝑘) = (𝐺𝑋))
206205eqeq1d 2762 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑋 → ((𝐺𝑘) = ∅ ↔ (𝐺𝑋) = ∅))
207204, 206syl5ibrcom 237 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺𝑘) = ∅))
208 eldifi 3875 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘𝐵)
209208adantl 473 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘𝐵)
2107adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌𝐴)
211210, 113, 114sylancl 697 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) ∈ V)
212209, 211, 119syl2anc 696 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)))
213 ssid 3765 . . . . . . . . . . . . . . . . . . 19 (𝐹 supp ∅) ⊆ (𝐹 supp ∅)
214213a1i 11 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
21530, 214, 3, 13suppssr 7496 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹𝑘) = ∅)
216212, 215eqtr3d 2796 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅)
217 iffalse 4239 . . . . . . . . . . . . . . . . 17 𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = (𝐺𝑘))
218217eqeq1d 2762 . . . . . . . . . . . . . . . 16 𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺𝑘)) = ∅ ↔ (𝐺𝑘) = ∅))
219216, 218syl5ibcom 235 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺𝑘) = ∅))
220207, 219pm2.61d 170 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺𝑘) = ∅)
22127, 220suppss 7495 . . . . . . . . . . . . 13 (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅))
222 reldisj 4163 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
223221, 222syl 17 . . . . . . . . . . . 12 (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})))
224186, 223mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))
225 uncom 3900 . . . . . . . . . . . . 13 ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅))
226137, 225syl6sseq 3792 . . . . . . . . . . . 12 (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)))
227 ssundif 4196 . . . . . . . . . . . 12 ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
228226, 227sylib 208 . . . . . . . . . . 11 (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅))
229224, 228eqssd 3761 . . . . . . . . . 10 (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋}))
230165, 183, 2293eqtr4rd 2805 . . . . . . . . 9 (𝜑 → (𝐺 supp ∅) = (𝑂 dom 𝑂))
231 isores3 6749 . . . . . . . . 9 ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 dom 𝑂)) → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
23237, 154, 230, 231syl3anc 1477 . . . . . . . 8 (𝜑 → (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅)))
233 cantnfp1.k . . . . . . . . . . 11 𝐾 = OrdIso( E , (𝐺 supp ∅))
2341, 2, 3, 233, 5cantnfcl 8739 . . . . . . . . . 10 (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω))
235234simpld 477 . . . . . . . . 9 (𝜑 → E We (𝐺 supp ∅))
236 epse 5249 . . . . . . . . 9 E Se (𝐺 supp ∅)
237233oieu 8611 . . . . . . . . 9 (( E We (𝐺 supp ∅) ∧ E Se (𝐺 supp ∅)) → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
238235, 236, 237sylancl 697 . . . . . . . 8 (𝜑 → ((Ord dom 𝑂 ∧ (𝑂 dom 𝑂) Isom E , E ( dom 𝑂, (𝐺 supp ∅))) ↔ ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾)))
239152, 232, 238mpbi2and 994 . . . . . . 7 (𝜑 → ( dom 𝑂 = dom 𝐾 ∧ (𝑂 dom 𝑂) = 𝐾))
240239simpld 477 . . . . . 6 (𝜑 dom 𝑂 = dom 𝐾)
241240fveq2d 6357 . . . . 5 (𝜑 → (𝑀 dom 𝑂) = (𝑀‘dom 𝐾))
242 eleq1 2827 . . . . . . . . . 10 (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
243 fveq2 6353 . . . . . . . . . . 11 (𝑥 = ∅ → (𝐻𝑥) = (𝐻‘∅))
244 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = ∅ → (𝑀𝑥) = (𝑀‘∅))
245 cantnfp1.m . . . . . . . . . . . . . 14 𝑀 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴𝑜 (𝐾𝑘)) ·𝑜 (𝐺‘(𝐾𝑘))) +𝑜 𝑧)), ∅)
246245seqom0g 7721 . . . . . . . . . . . . 13 (∅ ∈ V → (𝑀‘∅) = ∅)
24754, 246ax-mp 5 . . . . . . . . . . . 12 (𝑀‘∅) = ∅
248244, 247syl6eq 2810 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑀𝑥) = ∅)
249243, 248eqeq12d 2775 . . . . . . . . . 10 (𝑥 = ∅ → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻‘∅) = ∅))
250242, 249imbi12d 333 . . . . . . . . 9 (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)))
251250imbi2d 329 . . . . . . . 8 (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))))
252 eleq1 2827 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
253 fveq2 6353 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝐻𝑥) = (𝐻𝑦))
254 fveq2 6353 . . . . . . . . . . 11 (𝑥 = 𝑦 → (𝑀𝑥) = (𝑀𝑦))
255253, 254eqeq12d 2775 . . . . . . . . . 10 (𝑥 = 𝑦 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻𝑦) = (𝑀𝑦)))
256252, 255imbi12d 333 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
257256imbi2d 329 . . . . . . . 8 (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)))))
258 eleq1 2827 . . . . . . . . . 10 (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂))
259 fveq2 6353 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝐻𝑥) = (𝐻‘suc 𝑦))
260 fveq2 6353 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑀𝑥) = (𝑀‘suc 𝑦))
261259, 260eqeq12d 2775 . . . . . . . . . 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 2827 . . . . . . . . . 10 (𝑥 = dom 𝑂 → (𝑥 ∈ dom 𝑂 dom 𝑂 ∈ dom 𝑂))
265 fveq2 6353 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝐻𝑥) = (𝐻 dom 𝑂))
266 fveq2 6353 . . . . . . . . . . 11 (𝑥 = dom 𝑂 → (𝑀𝑥) = (𝑀 dom 𝑂))
267265, 266eqeq12d 2775 . . . . . . . . . 10 (𝑥 = dom 𝑂 → ((𝐻𝑥) = (𝑀𝑥) ↔ (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
268264, 267imbi12d 333 . . . . . . . . 9 (𝑥 = dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥)) ↔ ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
269268imbi2d 329 . . . . . . . 8 (𝑥 = dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻𝑥) = (𝑀𝑥))) ↔ (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))))
27011seqom0g 7721 . . . . . . . . . 10 (∅ ∈ V → (𝐻‘∅) = ∅)
27154, 270mp1i 13 . . . . . . . . 9 (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)
272271a1i 11 . . . . . . . 8 (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅))
273 nnord 7239 . . . . . . . . . . . . . . . 16 (dom 𝑂 ∈ ω → Ord dom 𝑂)
27417, 273syl 17 . . . . . . . . . . . . . . 15 (𝜑 → Ord dom 𝑂)
275 ordtr 5898 . . . . . . . . . . . . . . 15 (Ord dom 𝑂 → Tr dom 𝑂)
276274, 275syl 17 . . . . . . . . . . . . . 14 (𝜑 → Tr dom 𝑂)
277 trsuc 5971 . . . . . . . . . . . . . 14 ((Tr dom 𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
278276, 277sylan 489 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂)
279278ex 449 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂𝑦 ∈ dom 𝑂))
280279imim1d 82 . . . . . . . . . . 11 (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦))))
281 oveq2 6822 . . . . . . . . . . . . . 14 ((𝐻𝑦) = (𝑀𝑦) → (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
282 elnn 7241 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω)
283282ancoms 468 . . . . . . . . . . . . . . . . . 18 ((dom 𝑂 ∈ ω ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
28417, 283sylan 489 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
285278, 284syldan 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω)
2861, 2, 3, 4, 10, 11cantnfsuc 8742 . . . . . . . . . . . . . . . 16 ((𝜑𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
287285, 286syldan 488 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)))
2881, 2, 3, 233, 5, 245cantnfsuc 8742 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
289285, 288syldan 488 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)))
290239simprd 482 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝑂 dom 𝑂) = 𝐾)
291290fveq1d 6355 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
292291adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝐾𝑦))
29314eleq2d 2825 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
294293biimpa 502 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc dom 𝑂)
295152adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord dom 𝑂)
296 ordsucelsuc 7188 . . . . . . . . . . . . . . . . . . . . . . 23 (Ord dom 𝑂 → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
297295, 296syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 dom 𝑂 ↔ suc 𝑦 ∈ suc dom 𝑂))
298294, 297mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 dom 𝑂)
299 fvres 6369 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 dom 𝑂 → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
300298, 299syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 dom 𝑂)‘𝑦) = (𝑂𝑦))
301292, 300eqtr3d 2796 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) = (𝑂𝑦))
302301oveq2d 6830 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴𝑜 (𝐾𝑦)) = (𝐴𝑜 (𝑂𝑦)))
303 suppssdm 7477 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐺 supp ∅) ⊆ dom 𝐺
304 fdm 6212 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐺:𝐵𝐴 → dom 𝐺 = 𝐵)
30527, 304syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → dom 𝐺 = 𝐵)
306303, 305syl5sseq 3794 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
307306adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵)
308240adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → dom 𝑂 = dom 𝐾)
309298, 308eleqtrd 2841 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾)
310233oif 8602 . . . . . . . . . . . . . . . . . . . . . . 23 𝐾:dom 𝐾⟶(𝐺 supp ∅)
311310ffvelrni 6522 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 ∈ dom 𝐾 → (𝐾𝑦) ∈ (𝐺 supp ∅))
312309, 311syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ (𝐺 supp ∅))
313307, 312sseldd 3745 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾𝑦) ∈ 𝐵)
3147adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌𝐴)
315 fvex 6363 . . . . . . . . . . . . . . . . . . . . 21 (𝐺‘(𝐾𝑦)) ∈ V
316 ifexg 4301 . . . . . . . . . . . . . . . . . . . . 21 ((𝑌𝐴 ∧ (𝐺‘(𝐾𝑦)) ∈ V) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
317314, 315, 316sylancl 697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V)
318 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝑡 = 𝑋 ↔ (𝐾𝑦) = 𝑋))
319 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑡 = (𝐾𝑦) → (𝐺𝑡) = (𝐺‘(𝐾𝑦)))
320318, 319ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . 21 (𝑡 = (𝐾𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺𝑡)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
321320, 9fvmptg 6443 . . . . . . . . . . . . . . . . . . . 20 (((𝐾𝑦) ∈ 𝐵 ∧ if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) ∈ V) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
322313, 317, 321syl2anc 696 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))))
323301fveq2d 6357 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
324184adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅))
325 nelneq 2863 . . . . . . . . . . . . . . . . . . . . 21 (((𝐾𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾𝑦) = 𝑋)
326312, 324, 325syl2anc 696 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾𝑦) = 𝑋)
327326iffalsed 4241 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾𝑦))) = (𝐺‘(𝐾𝑦)))
328322, 323, 3273eqtr3rd 2803 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾𝑦)) = (𝐹‘(𝑂𝑦)))
329302, 328oveq12d 6832 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) = ((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))))
330329oveq1d 6829 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴𝑜 (𝐾𝑦)) ·𝑜 (𝐺‘(𝐾𝑦))) +𝑜 (𝑀𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
331289, 330eqtrd 2794 . . . . . . . . . . . . . . 15 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦)))
332287, 331eqeq12d 2775 . . . . . . . . . . . . . 14 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝐻𝑦)) = (((𝐴𝑜 (𝑂𝑦)) ·𝑜 (𝐹‘(𝑂𝑦))) +𝑜 (𝑀𝑦))))
333281, 332syl5ibr 236 . . . . . . . . . . . . 13 ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))
334333ex 449 . . . . . . . . . . . 12 (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻𝑦) = (𝑀𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
335334a2d 29 . . . . . . . . . . 11 (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻𝑦) = (𝑀𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))
336280, 335syld 47 . . . . . . . . . 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 7258 . . . . . . 7 ( dom 𝑂 ∈ ω → (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))))
34020, 339mpcom 38 . . . . . 6 (𝜑 → ( dom 𝑂 ∈ dom 𝑂 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂)))
34172, 340mpd 15 . . . . 5 (𝜑 → (𝐻 dom 𝑂) = (𝑀 dom 𝑂))
3421, 2, 3, 233, 5, 245cantnfval 8740 . . . . 5 (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾))
343241, 341, 3423eqtr4d 2804 . . . 4 (𝜑 → (𝐻 dom 𝑂) = ((𝐴 CNF 𝐵)‘𝐺))
344150, 343oveq12d 6832 . . 3 (𝜑 → (((𝐴𝑜 (𝑂 dom 𝑂)) ·𝑜 (𝐹‘(𝑂 dom 𝑂))) +𝑜 (𝐻 dom 𝑂)) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
34522, 344eqtrd 2794 . 2 (𝜑 → (𝐻‘suc dom 𝑂) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
34612, 15, 3453eqtrd 2798 1 (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴𝑜 𝑋) ·𝑜 𝑌) +𝑜 ((𝐴 CNF 𝐵)‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1632  wcel 2139  wne 2932  Vcvv 3340  cdif 3712  cun 3713  cin 3714  wss 3715  c0 4058  ifcif 4230  {csn 4321   cuni 4588   class class class wbr 4804  cmpt 4881  Tr wtr 4904   E cep 5178   Se wse 5223   We wwe 5224  ccnv 5265  dom cdm 5266  cres 5268  cima 5269  Ord word 5883  Oncon0 5884  suc csuc 5886  Fun wfun 6043   Fn wfn 6044  wf 6045  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049   Isom wiso 6050  (class class class)co 6814  cmpt2 6816  ωcom 7231   supp csupp 7464  seq𝜔cseqom 7712  1𝑜c1o 7723   +𝑜 coa 7727   ·𝑜 comu 7728  𝑜 coe 7729   finSupp cfsupp 8442  OrdIsocoi 8581   CNF ccnf 8733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-seqom 7713  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-oi 8582  df-cnf 8734
This theorem is referenced by:  cantnfp1  8753
  Copyright terms: Public domain W3C validator