| Step | Hyp | Ref | 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(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) | 
| 10 | 1, 2, 3, 5, 6, 7, 8, 9 | cantnfp1lem1 9719 | . . 3
⊢ (𝜑 → 𝐹 ∈ 𝑆) | 
| 11 |  | cantnfp1.h | . . 3
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐹‘(𝑂‘𝑘))) +o 𝑧)), ∅) | 
| 12 | 1, 2, 3, 4, 10, 11 | cantnfval 9709 | . 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂)) | 
| 13 |  | cantnfp1.e | . . . 4
⊢ (𝜑 → ∅ ∈ 𝑌) | 
| 14 | 1, 2, 3, 5, 6, 7, 8, 9, 13, 4 | cantnfp1lem2 9720 | . . 3
⊢ (𝜑 → dom 𝑂 = suc ∪ dom
𝑂) | 
| 15 | 14 | fveq2d 6909 | . 2
⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom
𝑂)) | 
| 16 | 1, 2, 3, 4, 10 | cantnfcl 9708 | . . . . . . 7
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω)) | 
| 17 | 16 | simprd 495 | . . . . . 6
⊢ (𝜑 → dom 𝑂 ∈ ω) | 
| 18 | 14, 17 | eqeltrrd 2841 | . . . . 5
⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω) | 
| 19 |  | peano2b 7905 | . . . . 5
⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω) | 
| 20 | 18, 19 | sylibr 234 | . . . 4
⊢ (𝜑 → ∪ dom 𝑂 ∈ ω) | 
| 21 | 1, 2, 3, 4, 10, 11 | cantnfsuc 9711 | . . . 4
⊢ ((𝜑 ∧ ∪ dom 𝑂 ∈ ω) → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑o (𝑂‘∪ dom
𝑂)) ·o
(𝐹‘(𝑂‘∪ dom
𝑂))) +o (𝐻‘∪ dom 𝑂))) | 
| 22 | 20, 21 | mpdan 687 | . . 3
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑o (𝑂‘∪ dom
𝑂)) ·o
(𝐹‘(𝑂‘∪ dom
𝑂))) +o (𝐻‘∪ dom 𝑂))) | 
| 23 |  | ovexd 7467 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) | 
| 24 | 16 | simpld 494 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → E We (𝐹 supp ∅)) | 
| 25 | 4 | oiiso 9578 | . . . . . . . . . . . . . . 15
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅))) | 
| 26 | 23, 24, 25 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅))) | 
| 27 |  | isof1o 7344 | . . . . . . . . . . . . . 14
⊢ (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅)) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅)) | 
| 29 |  | f1ocnv 6859 | . . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) → ◡𝑂:(𝐹 supp ∅)–1-1-onto→dom
𝑂) | 
| 30 |  | f1of 6847 | . . . . . . . . . . . . 13
⊢ (◡𝑂:(𝐹 supp ∅)–1-1-onto→dom
𝑂 → ◡𝑂:(𝐹 supp ∅)⟶dom 𝑂) | 
| 31 | 28, 29, 30 | 3syl 18 | . . . . . . . . . . . 12
⊢ (𝜑 → ◡𝑂:(𝐹 supp ∅)⟶dom 𝑂) | 
| 32 |  | iftrue 4530 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = 𝑌) | 
| 33 | 9, 32, 6, 7 | fvmptd3 7038 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝑋) = 𝑌) | 
| 34 | 13 | ne0d 4341 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ≠ ∅) | 
| 35 | 33, 34 | eqnetrd 3007 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑋) ≠ ∅) | 
| 36 | 7 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → 𝑌 ∈ 𝐴) | 
| 37 | 1, 2, 3 | cantnfs 9707 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) | 
| 38 | 5, 37 | mpbid 232 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) | 
| 39 | 38 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) | 
| 40 | 39 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → (𝐺‘𝑡) ∈ 𝐴) | 
| 41 | 36, 40 | ifcld 4571 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) ∈ 𝐴) | 
| 42 | 41, 9 | fmptd 7133 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) | 
| 43 | 42 | ffnd 6736 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 Fn 𝐵) | 
| 44 |  | 0ex 5306 | . . . . . . . . . . . . . . 15
⊢ ∅
∈ V | 
| 45 | 44 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈
V) | 
| 46 |  | elsuppfn 8196 | . . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) | 
| 47 | 43, 3, 45, 46 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) | 
| 48 | 6, 35, 47 | mpbir2and 713 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (𝐹 supp ∅)) | 
| 49 | 31, 48 | ffvelcdmd 7104 | . . . . . . . . . . 11
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂) | 
| 50 |  | elssuni 4936 | . . . . . . . . . . 11
⊢ ((◡𝑂‘𝑋) ∈ dom 𝑂 → (◡𝑂‘𝑋) ⊆ ∪ dom
𝑂) | 
| 51 | 49, 50 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (◡𝑂‘𝑋) ⊆ ∪ dom
𝑂) | 
| 52 | 4 | oicl 9570 | . . . . . . . . . . . 12
⊢ Ord dom
𝑂 | 
| 53 |  | ordelon 6407 | . . . . . . . . . . . 12
⊢ ((Ord dom
𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On) | 
| 54 | 52, 49, 53 | sylancr 587 | . . . . . . . . . . 11
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On) | 
| 55 |  | nnon 7894 | . . . . . . . . . . . 12
⊢ (∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ On) | 
| 56 | 20, 55 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ∪ dom 𝑂 ∈ On) | 
| 57 |  | ontri1 6417 | . . . . . . . . . . 11
⊢ (((◡𝑂‘𝑋) ∈ On ∧ ∪ dom 𝑂 ∈ On) → ((◡𝑂‘𝑋) ⊆ ∪ dom
𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))) | 
| 58 | 54, 56, 57 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → ((◡𝑂‘𝑋) ⊆ ∪ dom
𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))) | 
| 59 | 51, 58 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)) | 
| 60 |  | sucidg 6464 | . . . . . . . . . . . . . 14
⊢ (∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ suc ∪ dom
𝑂) | 
| 61 | 20, 60 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∪ dom 𝑂 ∈ suc ∪ dom
𝑂) | 
| 62 | 61, 14 | eleqtrrd 2843 | . . . . . . . . . . . 12
⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂) | 
| 63 |  | isorel 7347 | . . . . . . . . . . . 12
⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom
𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) E (𝑂‘(◡𝑂‘𝑋)))) | 
| 64 | 26, 62, 49, 63 | syl12anc 836 | . . . . . . . . . . 11
⊢ (𝜑 → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) E (𝑂‘(◡𝑂‘𝑋)))) | 
| 65 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (◡𝑂‘𝑋) ∈ V | 
| 66 | 65 | epeli 5585 | . . . . . . . . . . 11
⊢ (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ ∪ dom
𝑂 ∈ (◡𝑂‘𝑋)) | 
| 67 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V | 
| 68 | 67 | epeli 5585 | . . . . . . . . . . 11
⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋))) | 
| 69 | 64, 66, 68 | 3bitr3g 313 | . . . . . . . . . 10
⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)))) | 
| 70 |  | f1ocnvfv2 7298 | . . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) | 
| 71 | 28, 48, 70 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) | 
| 72 | 71 | eleq2d 2826 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom
𝑂) ∈ 𝑋)) | 
| 73 | 69, 72 | bitrd 279 | . . . . . . . . 9
⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) ∈ 𝑋)) | 
| 74 | 59, 73 | mtbid 324 | . . . . . . . 8
⊢ (𝜑 → ¬ (𝑂‘∪ dom
𝑂) ∈ 𝑋) | 
| 75 | 8 | sseld 3981 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) → (𝑂‘∪ dom 𝑂) ∈ 𝑋)) | 
| 76 |  | suppssdm 8203 | . . . . . . . . . . . . . . . 16
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 | 
| 77 | 76, 42 | fssdm 6754 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵) | 
| 78 |  | onss 7806 | . . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) | 
| 79 | 3, 78 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆ On) | 
| 80 | 77, 79 | sstrd 3993 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 supp ∅) ⊆ On) | 
| 81 | 4 | oif 9571 | . . . . . . . . . . . . . . . 16
⊢ 𝑂:dom 𝑂⟶(𝐹 supp ∅) | 
| 82 | 81 | ffvelcdmi 7102 | . . . . . . . . . . . . . . 15
⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom
𝑂) ∈ (𝐹 supp ∅)) | 
| 83 | 62, 82 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈ (𝐹 supp ∅)) | 
| 84 | 80, 83 | sseldd 3983 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈
On) | 
| 85 |  | eloni 6393 | . . . . . . . . . . . . 13
⊢ ((𝑂‘∪ dom 𝑂) ∈ On → Ord (𝑂‘∪ dom
𝑂)) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → Ord (𝑂‘∪ dom
𝑂)) | 
| 87 |  | ordn2lp 6403 | . . . . . . . . . . . 12
⊢ (Ord
(𝑂‘∪ dom 𝑂) → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 88 | 86, 87 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 89 |  | imnan 399 | . . . . . . . . . . 11
⊢ (((𝑂‘∪ dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) ↔ ¬ ((𝑂‘∪ dom 𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 90 | 88, 89 | sylibr 234 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 91 | 75, 90 | syld 47 | . . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) → ¬
𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 92 |  | onelon 6408 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) | 
| 93 | 3, 6, 92 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ On) | 
| 94 |  | eloni 6393 | . . . . . . . . . . . 12
⊢ (𝑋 ∈ On → Ord 𝑋) | 
| 95 | 93, 94 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → Ord 𝑋) | 
| 96 |  | ordirr 6401 | . . . . . . . . . . 11
⊢ (Ord
𝑋 → ¬ 𝑋 ∈ 𝑋) | 
| 97 | 95, 96 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑋) | 
| 98 |  | elsni 4642 | . . . . . . . . . . . 12
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (𝑂‘∪ dom
𝑂) = 𝑋) | 
| 99 | 98 | eleq2d 2826 | . . . . . . . . . . 11
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂‘∪ dom
𝑂) ↔ 𝑋 ∈ 𝑋)) | 
| 100 | 99 | notbid 318 | . . . . . . . . . 10
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂) ↔ ¬ 𝑋 ∈ 𝑋)) | 
| 101 | 97, 100 | syl5ibrcom 247 | . . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 102 |  | eqeq1 2740 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑘 → (𝑡 = 𝑋 ↔ 𝑘 = 𝑋)) | 
| 103 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑘 → (𝐺‘𝑡) = (𝐺‘𝑘)) | 
| 104 | 102, 103 | ifbieq2d 4551 | . . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) | 
| 105 |  | eldifi 4130 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ 𝐵) | 
| 106 | 105 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘 ∈ 𝐵) | 
| 107 | 7 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌 ∈ 𝐴) | 
| 108 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (𝐺‘𝑘) ∈ V | 
| 109 |  | ifexg 4574 | . . . . . . . . . . . . . . 15
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐺‘𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) | 
| 110 | 107, 108,
109 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) | 
| 111 | 9, 104, 106, 110 | fvmptd3 7038 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) | 
| 112 |  | eldifn 4131 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 113 | 112 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 114 |  | velsn 4641 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋) | 
| 115 |  | elun2 4182 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 116 | 114, 115 | sylbir 235 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑋 → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 117 | 113, 116 | nsyl 140 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋) | 
| 118 | 117 | iffalsed 4535 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = (𝐺‘𝑘)) | 
| 119 |  | ssun1 4177 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) | 
| 120 |  | sscon 4142 | . . . . . . . . . . . . . . . 16
⊢ ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))) | 
| 121 | 119, 120 | ax-mp 5 | . . . . . . . . . . . . . . 15
⊢ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)) | 
| 122 | 121 | sseli 3978 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) | 
| 123 |  | ssidd 4006 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅)) | 
| 124 | 39, 123, 3, 13 | suppssr 8221 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑘) = ∅) | 
| 125 | 122, 124 | sylan2 593 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺‘𝑘) = ∅) | 
| 126 | 111, 118,
125 | 3eqtrd 2780 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = ∅) | 
| 127 | 42, 126 | suppss 8220 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 128 | 127, 83 | sseldd 3983 | . . . . . . . . . 10
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋})) | 
| 129 |  | elun 4152 | . . . . . . . . . 10
⊢ ((𝑂‘∪ dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂‘∪ dom 𝑂) ∈ {𝑋})) | 
| 130 | 128, 129 | sylib 218 | . . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂‘∪ dom 𝑂) ∈ {𝑋})) | 
| 131 | 91, 101, 130 | mpjaod 860 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) | 
| 132 |  | ioran 985 | . . . . . . . 8
⊢ (¬
((𝑂‘∪ dom 𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) ↔ (¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 133 | 74, 131, 132 | sylanbrc 583 | . . . . . . 7
⊢ (𝜑 → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) | 
| 134 |  | ordtri3 6419 | . . . . . . . 8
⊢ ((Ord
(𝑂‘∪ dom 𝑂) ∧ Ord 𝑋) → ((𝑂‘∪ dom
𝑂) = 𝑋 ↔ ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)))) | 
| 135 | 86, 95, 134 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) = 𝑋 ↔ ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)))) | 
| 136 | 133, 135 | mpbird 257 | . . . . . 6
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) = 𝑋) | 
| 137 | 136 | oveq2d 7448 | . . . . 5
⊢ (𝜑 → (𝐴 ↑o (𝑂‘∪ dom
𝑂)) = (𝐴 ↑o 𝑋)) | 
| 138 | 136 | fveq2d 6909 | . . . . . 6
⊢ (𝜑 → (𝐹‘(𝑂‘∪ dom
𝑂)) = (𝐹‘𝑋)) | 
| 139 | 138, 33 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → (𝐹‘(𝑂‘∪ dom
𝑂)) = 𝑌) | 
| 140 | 137, 139 | oveq12d 7450 | . . . 4
⊢ (𝜑 → ((𝐴 ↑o (𝑂‘∪ dom
𝑂)) ·o
(𝐹‘(𝑂‘∪ dom
𝑂))) = ((𝐴 ↑o 𝑋) ·o 𝑌)) | 
| 141 |  | nnord 7896 | . . . . . . . . 9
⊢ (∪ dom 𝑂 ∈ ω → Ord ∪ dom 𝑂) | 
| 142 | 20, 141 | syl 17 | . . . . . . . 8
⊢ (𝜑 → Ord ∪ dom 𝑂) | 
| 143 |  | sssucid 6463 | . . . . . . . . . 10
⊢ ∪ dom 𝑂 ⊆ suc ∪
dom 𝑂 | 
| 144 | 143, 14 | sseqtrrid 4026 | . . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑂 ⊆ dom 𝑂) | 
| 145 |  | f1ofo 6854 | . . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂–onto→(𝐹 supp ∅)) | 
| 146 | 28, 145 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑂:dom 𝑂–onto→(𝐹 supp ∅)) | 
| 147 |  | foima 6824 | . . . . . . . . . . . 12
⊢ (𝑂:dom 𝑂–onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅)) | 
| 148 | 146, 147 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅)) | 
| 149 |  | ffn 6735 | . . . . . . . . . . . . . 14
⊢ (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂) | 
| 150 | 81, 149 | ax-mp 5 | . . . . . . . . . . . . 13
⊢ 𝑂 Fn dom 𝑂 | 
| 151 |  | fnsnfv 6987 | . . . . . . . . . . . . 13
⊢ ((𝑂 Fn dom 𝑂 ∧ ∪ dom
𝑂 ∈ dom 𝑂) → {(𝑂‘∪ dom
𝑂)} = (𝑂 “ {∪ dom
𝑂})) | 
| 152 | 150, 62, 151 | sylancr 587 | . . . . . . . . . . . 12
⊢ (𝜑 → {(𝑂‘∪ dom
𝑂)} = (𝑂 “ {∪ dom
𝑂})) | 
| 153 | 136 | sneqd 4637 | . . . . . . . . . . . 12
⊢ (𝜑 → {(𝑂‘∪ dom
𝑂)} = {𝑋}) | 
| 154 | 152, 153 | eqtr3d 2778 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ {∪ dom
𝑂}) = {𝑋}) | 
| 155 | 148, 154 | difeq12d 4126 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂})) = ((𝐹 supp ∅) ∖ {𝑋})) | 
| 156 |  | ordirr 6401 | . . . . . . . . . . . . . . . . 17
⊢ (Ord
∪ dom 𝑂 → ¬ ∪
dom 𝑂 ∈ ∪ dom 𝑂) | 
| 157 | 142, 156 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ ∪ dom
𝑂) | 
| 158 |  | disjsn 4710 | . . . . . . . . . . . . . . . 16
⊢ ((∪ dom 𝑂 ∩ {∪ dom
𝑂}) = ∅ ↔ ¬
∪ dom 𝑂 ∈ ∪ dom
𝑂) | 
| 159 | 157, 158 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (∪ dom 𝑂 ∩ {∪ dom
𝑂}) =
∅) | 
| 160 |  | disj3 4453 | . . . . . . . . . . . . . . 15
⊢ ((∪ dom 𝑂 ∩ {∪ dom
𝑂}) = ∅ ↔ ∪ dom 𝑂 = (∪ dom 𝑂 ∖ {∪ dom 𝑂})) | 
| 161 | 159, 160 | sylib 218 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ dom 𝑂 = (∪ dom 𝑂 ∖ {∪ dom 𝑂})) | 
| 162 |  | difun2 4480 | . . . . . . . . . . . . . 14
⊢ ((∪ dom 𝑂 ∪ {∪ dom
𝑂}) ∖ {∪ dom 𝑂}) = (∪ dom 𝑂 ∖ {∪ dom 𝑂}) | 
| 163 | 161, 162 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∪ dom 𝑂 = ((∪ dom 𝑂 ∪ {∪ dom 𝑂}) ∖ {∪ dom
𝑂})) | 
| 164 |  | df-suc 6389 | . . . . . . . . . . . . . . 15
⊢ suc ∪ dom 𝑂 = (∪ dom 𝑂 ∪ {∪ dom 𝑂}) | 
| 165 | 14, 164 | eqtrdi 2792 | . . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑂 = (∪ dom 𝑂 ∪ {∪ dom 𝑂})) | 
| 166 | 165 | difeq1d 4124 | . . . . . . . . . . . . 13
⊢ (𝜑 → (dom 𝑂 ∖ {∪ dom
𝑂}) = ((∪ dom 𝑂 ∪ {∪ dom
𝑂}) ∖ {∪ dom 𝑂})) | 
| 167 | 163, 166 | eqtr4d 2779 | . . . . . . . . . . . 12
⊢ (𝜑 → ∪ dom 𝑂 = (dom 𝑂 ∖ {∪ dom
𝑂})) | 
| 168 | 167 | imaeq2d 6077 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ ∪ dom
𝑂) = (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂}))) | 
| 169 |  | dff1o3 6853 | . . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂–onto→(𝐹 supp ∅) ∧ Fun ◡𝑂)) | 
| 170 | 169 | simprbi 496 | . . . . . . . . . . . 12
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) → Fun ◡𝑂) | 
| 171 |  | imadif 6649 | . . . . . . . . . . . 12
⊢ (Fun
◡𝑂 → (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) | 
| 172 | 28, 170, 171 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) | 
| 173 | 168, 172 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (𝑂 “ ∪ dom
𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) | 
| 174 | 8, 97 | ssneldd 3985 | . . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅)) | 
| 175 |  | disjsn 4710 | . . . . . . . . . . . . 13
⊢ (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅)) | 
| 176 | 174, 175 | sylibr 234 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅) | 
| 177 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺‘𝑋) ∈ V | 
| 178 |  | dif1o 8539 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1o) ↔
((𝐺‘𝑋) ∈ V ∧ (𝐺‘𝑋) ≠ ∅)) | 
| 179 | 177, 178 | mpbiran 709 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1o) ↔
(𝐺‘𝑋) ≠ ∅) | 
| 180 | 39 | ffnd 6736 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐺 Fn 𝐵) | 
| 181 |  | elsuppfn 8196 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) | 
| 182 | 180, 3, 45, 181 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) | 
| 183 | 179 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐺‘𝑋) ∈ (V ∖ 1o) ↔
(𝐺‘𝑋) ≠ ∅)) | 
| 184 | 183 | bicomd 223 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ ↔ (𝐺‘𝑋) ∈ (V ∖
1o))) | 
| 185 | 184 | anbi2d 630 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1o)))) | 
| 186 | 182, 185 | bitrd 279 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1o)))) | 
| 187 | 8 | sseld 3981 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋 ∈ 𝑋)) | 
| 188 | 186, 187 | sylbird 260 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖ 1o)) →
𝑋 ∈ 𝑋)) | 
| 189 | 6, 188 | mpand 695 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺‘𝑋) ∈ (V ∖ 1o) →
𝑋 ∈ 𝑋)) | 
| 190 | 179, 189 | biimtrrid 243 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ → 𝑋 ∈ 𝑋)) | 
| 191 | 190 | necon1bd 2957 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 𝑋 ∈ 𝑋 → (𝐺‘𝑋) = ∅)) | 
| 192 | 97, 191 | mpd 15 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺‘𝑋) = ∅) | 
| 193 | 192 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺‘𝑋) = ∅) | 
| 194 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑋 → ((𝐺‘𝑘) = ∅ ↔ (𝐺‘𝑋) = ∅)) | 
| 195 | 193, 194 | syl5ibrcom 247 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺‘𝑘) = ∅)) | 
| 196 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘 ∈ 𝐵) | 
| 197 | 196 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘 ∈ 𝐵) | 
| 198 | 7 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌 ∈ 𝐴) | 
| 199 | 198, 108,
109 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) | 
| 200 | 9, 104, 197, 199 | fvmptd3 7038 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) | 
| 201 |  | ssidd 4006 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅)) | 
| 202 | 42, 201, 3, 13 | suppssr 8221 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑘) = ∅) | 
| 203 | 200, 202 | eqtr3d 2778 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = ∅) | 
| 204 |  | iffalse 4533 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = (𝐺‘𝑘)) | 
| 205 | 204 | eqeq1d 2738 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = ∅ ↔ (𝐺‘𝑘) = ∅)) | 
| 206 | 203, 205 | syl5ibcom 245 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺‘𝑘) = ∅)) | 
| 207 | 195, 206 | pm2.61d 179 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺‘𝑘) = ∅) | 
| 208 | 39, 207 | suppss 8220 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅)) | 
| 209 |  | reldisj 4452 | . . . . . . . . . . . . 13
⊢ ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))) | 
| 210 | 208, 209 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))) | 
| 211 | 176, 210 | mpbid 232 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})) | 
| 212 |  | uncom 4157 | . . . . . . . . . . . . 13
⊢ ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅)) | 
| 213 | 127, 212 | sseqtrdi 4023 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅))) | 
| 214 |  | ssundif 4487 | . . . . . . . . . . . 12
⊢ ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅)) | 
| 215 | 213, 214 | sylib 218 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅)) | 
| 216 | 211, 215 | eqssd 4000 | . . . . . . . . . 10
⊢ (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋})) | 
| 217 | 155, 173,
216 | 3eqtr4rd 2787 | . . . . . . . . 9
⊢ (𝜑 → (𝐺 supp ∅) = (𝑂 “ ∪ dom
𝑂)) | 
| 218 |  | isores3 7356 | . . . . . . . . 9
⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ∪ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 “ ∪ dom
𝑂)) → (𝑂 ↾ ∪ dom 𝑂) Isom E , E (∪
dom 𝑂, (𝐺 supp ∅))) | 
| 219 | 26, 144, 217, 218 | syl3anc 1372 | . . . . . . . 8
⊢ (𝜑 → (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) | 
| 220 |  | cantnfp1.k | . . . . . . . . . . 11
⊢ 𝐾 = OrdIso( E , (𝐺 supp ∅)) | 
| 221 | 1, 2, 3, 220, 5 | cantnfcl 9708 | . . . . . . . . . 10
⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω)) | 
| 222 | 221 | simpld 494 | . . . . . . . . 9
⊢ (𝜑 → E We (𝐺 supp ∅)) | 
| 223 |  | epse 5666 | . . . . . . . . 9
⊢  E Se
(𝐺 supp
∅) | 
| 224 | 220 | oieu 9580 | . . . . . . . . 9
⊢ (( E We
(𝐺 supp ∅) ∧ E Se
(𝐺 supp ∅)) →
((Ord ∪ dom 𝑂 ∧ (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) ↔ (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾))) | 
| 225 | 222, 223,
224 | sylancl 586 | . . . . . . . 8
⊢ (𝜑 → ((Ord ∪ dom 𝑂 ∧ (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) ↔ (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾))) | 
| 226 | 142, 219,
225 | mpbi2and 712 | . . . . . . 7
⊢ (𝜑 → (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾)) | 
| 227 | 226 | simpld 494 | . . . . . 6
⊢ (𝜑 → ∪ dom 𝑂 = dom 𝐾) | 
| 228 | 227 | fveq2d 6909 | . . . . 5
⊢ (𝜑 → (𝑀‘∪ dom
𝑂) = (𝑀‘dom 𝐾)) | 
| 229 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝑥 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂)) | 
| 230 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝐻‘𝑥) = (𝐻‘∅)) | 
| 231 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑀‘𝑥) = (𝑀‘∅)) | 
| 232 |  | cantnfp1.m | . . . . . . . . . . . . . 14
⊢ 𝑀 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐾‘𝑘)) ·o (𝐺‘(𝐾‘𝑘))) +o 𝑧)), ∅) | 
| 233 | 232 | seqom0g 8497 | . . . . . . . . . . . . 13
⊢ (∅
∈ V → (𝑀‘∅) = ∅) | 
| 234 | 44, 233 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (𝑀‘∅) =
∅ | 
| 235 | 231, 234 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑀‘𝑥) = ∅) | 
| 236 | 230, 235 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘∅) = ∅)) | 
| 237 | 229, 236 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) =
∅))) | 
| 238 | 237 | imbi2d 340 | . . . . . . . 8
⊢ (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) =
∅)))) | 
| 239 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂 ↔ 𝑦 ∈ dom 𝑂)) | 
| 240 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) | 
| 241 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) | 
| 242 | 240, 241 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘𝑦) = (𝑀‘𝑦))) | 
| 243 | 239, 242 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)))) | 
| 244 | 243 | imbi2d 340 | . . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))))) | 
| 245 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂)) | 
| 246 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝐻‘𝑥) = (𝐻‘suc 𝑦)) | 
| 247 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝑀‘𝑥) = (𝑀‘suc 𝑦)) | 
| 248 | 246, 247 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))) | 
| 249 | 245, 248 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) | 
| 250 | 249 | imbi2d 340 | . . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))) | 
| 251 |  | eleq1 2828 | . . . . . . . . . 10
⊢ (𝑥 = ∪
dom 𝑂 → (𝑥 ∈ dom 𝑂 ↔ ∪ dom
𝑂 ∈ dom 𝑂)) | 
| 252 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = ∪
dom 𝑂 → (𝐻‘𝑥) = (𝐻‘∪ dom
𝑂)) | 
| 253 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑥 = ∪
dom 𝑂 → (𝑀‘𝑥) = (𝑀‘∪ dom
𝑂)) | 
| 254 | 252, 253 | eqeq12d 2752 | . . . . . . . . . 10
⊢ (𝑥 = ∪
dom 𝑂 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))) | 
| 255 | 251, 254 | imbi12d 344 | . . . . . . . . 9
⊢ (𝑥 = ∪
dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)))) | 
| 256 | 255 | imbi2d 340 | . . . . . . . 8
⊢ (𝑥 = ∪
dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))))) | 
| 257 | 11 | seqom0g 8497 | . . . . . . . . 9
⊢ (∅
∈ dom 𝑂 → (𝐻‘∅) =
∅) | 
| 258 | 257 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)) | 
| 259 |  | nnord 7896 | . . . . . . . . . . . . . . . 16
⊢ (dom
𝑂 ∈ ω → Ord
dom 𝑂) | 
| 260 | 17, 259 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → Ord dom 𝑂) | 
| 261 |  | ordtr 6397 | . . . . . . . . . . . . . . 15
⊢ (Ord dom
𝑂 → Tr dom 𝑂) | 
| 262 | 260, 261 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Tr dom 𝑂) | 
| 263 |  | trsuc 6470 | . . . . . . . . . . . . . 14
⊢ ((Tr dom
𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂) | 
| 264 | 262, 263 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂) | 
| 265 | 264 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → 𝑦 ∈ dom 𝑂)) | 
| 266 | 265 | imim1d 82 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)))) | 
| 267 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑦) = (𝑀‘𝑦) → (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝐻‘𝑦)) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝑀‘𝑦))) | 
| 268 |  | elnn 7899 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω) | 
| 269 | 268 | ancoms 458 | . . . . . . . . . . . . . . . . 17
⊢ ((dom
𝑂 ∈ ω ∧
𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω) | 
| 270 | 17, 264, 269 | syl2an2r 685 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω) | 
| 271 | 1, 2, 3, 4, 10, 11 | cantnfsuc 9711 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝐻‘𝑦))) | 
| 272 | 270, 271 | syldan 591 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝐻‘𝑦))) | 
| 273 | 1, 2, 3, 220, 5, 232 | cantnfsuc 9711 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴 ↑o (𝐾‘𝑦)) ·o (𝐺‘(𝐾‘𝑦))) +o (𝑀‘𝑦))) | 
| 274 | 270, 273 | syldan 591 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴 ↑o (𝐾‘𝑦)) ·o (𝐺‘(𝐾‘𝑦))) +o (𝑀‘𝑦))) | 
| 275 | 226 | simprd 495 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑂 ↾ ∪ dom
𝑂) = 𝐾) | 
| 276 | 275 | fveq1d 6907 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝐾‘𝑦)) | 
| 277 | 276 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝐾‘𝑦)) | 
| 278 | 14 | eleq2d 2826 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc ∪ dom
𝑂)) | 
| 279 | 278 | biimpa 476 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc ∪ dom
𝑂) | 
| 280 | 142 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord ∪
dom 𝑂) | 
| 281 |  | ordsucelsuc 7843 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
∪ dom 𝑂 → (𝑦 ∈ ∪ dom
𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂)) | 
| 282 | 280, 281 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 ∈ ∪ dom
𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂)) | 
| 283 | 279, 282 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ∪ dom
𝑂) | 
| 284 | 283 | fvresd 6925 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝑂‘𝑦)) | 
| 285 | 277, 284 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) = (𝑂‘𝑦)) | 
| 286 | 285 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴 ↑o (𝐾‘𝑦)) = (𝐴 ↑o (𝑂‘𝑦))) | 
| 287 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑦) → (𝑡 = 𝑋 ↔ (𝐾‘𝑦) = 𝑋)) | 
| 288 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑦) → (𝐺‘𝑡) = (𝐺‘(𝐾‘𝑦))) | 
| 289 | 287, 288 | ifbieq2d 4551 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = (𝐾‘𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦)))) | 
| 290 |  | suppssdm 8203 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 | 
| 291 | 290, 39 | fssdm 6754 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) | 
| 292 | 291 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵) | 
| 293 | 227 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ∪ dom
𝑂 = dom 𝐾) | 
| 294 | 283, 293 | eleqtrd 2842 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾) | 
| 295 | 220 | oif 9571 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐾:dom 𝐾⟶(𝐺 supp ∅) | 
| 296 | 295 | ffvelcdmi 7102 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ dom 𝐾 → (𝐾‘𝑦) ∈ (𝐺 supp ∅)) | 
| 297 | 294, 296 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) ∈ (𝐺 supp ∅)) | 
| 298 | 292, 297 | sseldd 3983 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) ∈ 𝐵) | 
| 299 | 7 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌 ∈ 𝐴) | 
| 300 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺‘(𝐾‘𝑦)) ∈ V | 
| 301 |  | ifexg 4574 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐺‘(𝐾‘𝑦)) ∈ V) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) ∈ V) | 
| 302 | 299, 300,
301 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) ∈ V) | 
| 303 | 9, 289, 298, 302 | fvmptd3 7038 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾‘𝑦)) = if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦)))) | 
| 304 | 285 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾‘𝑦)) = (𝐹‘(𝑂‘𝑦))) | 
| 305 | 174 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅)) | 
| 306 |  | nelneq 2864 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾‘𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾‘𝑦) = 𝑋) | 
| 307 | 297, 305,
306 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾‘𝑦) = 𝑋) | 
| 308 | 307 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) = (𝐺‘(𝐾‘𝑦))) | 
| 309 | 303, 304,
308 | 3eqtr3rd 2785 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾‘𝑦)) = (𝐹‘(𝑂‘𝑦))) | 
| 310 | 286, 309 | oveq12d 7450 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴 ↑o (𝐾‘𝑦)) ·o (𝐺‘(𝐾‘𝑦))) = ((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦)))) | 
| 311 | 310 | oveq1d 7447 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴 ↑o (𝐾‘𝑦)) ·o (𝐺‘(𝐾‘𝑦))) +o (𝑀‘𝑦)) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝑀‘𝑦))) | 
| 312 | 274, 311 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝑀‘𝑦))) | 
| 313 | 272, 312 | eqeq12d 2752 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝐻‘𝑦)) = (((𝐴 ↑o (𝑂‘𝑦)) ·o (𝐹‘(𝑂‘𝑦))) +o (𝑀‘𝑦)))) | 
| 314 | 267, 313 | imbitrrid 246 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘𝑦) = (𝑀‘𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))) | 
| 315 | 314 | ex 412 | . . . . . . . . . . . 12
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻‘𝑦) = (𝑀‘𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) | 
| 316 | 315 | a2d 29 | . . . . . . . . . . 11
⊢ (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) | 
| 317 | 266, 316 | syld 47 | . . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) | 
| 318 | 317 | a2i 14 | . . . . . . . . 9
⊢ ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) | 
| 319 | 318 | a1i 11 | . . . . . . . 8
⊢ (𝑦 ∈ ω → ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))) | 
| 320 | 238, 244,
250, 256, 258, 319 | finds 7919 | . . . . . . 7
⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)))) | 
| 321 | 20, 320 | mpcom 38 | . . . . . 6
⊢ (𝜑 → (∪ dom 𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))) | 
| 322 | 62, 321 | mpd 15 | . . . . 5
⊢ (𝜑 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)) | 
| 323 | 1, 2, 3, 220, 5, 232 | cantnfval 9709 | . . . . 5
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾)) | 
| 324 | 228, 322,
323 | 3eqtr4d 2786 | . . . 4
⊢ (𝜑 → (𝐻‘∪ dom
𝑂) = ((𝐴 CNF 𝐵)‘𝐺)) | 
| 325 | 140, 324 | oveq12d 7450 | . . 3
⊢ (𝜑 → (((𝐴 ↑o (𝑂‘∪ dom
𝑂)) ·o
(𝐹‘(𝑂‘∪ dom
𝑂))) +o (𝐻‘∪ dom 𝑂)) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))) | 
| 326 | 22, 325 | eqtrd 2776 | . 2
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))) | 
| 327 | 12, 15, 326 | 3eqtrd 2780 | 1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑o 𝑋) ·o 𝑌) +o ((𝐴 CNF 𝐵)‘𝐺))) |