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 8458 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
11 | | cantnfp1.h |
. . 3
⊢ 𝐻 =
seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐹‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅) |
12 | 1, 2, 3, 4, 10, 11 | cantnfval 8448 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝑂)) |
13 | | cantnfp1.e |
. . . 4
⊢ (𝜑 → ∅ ∈ 𝑌) |
14 | 1, 2, 3, 5, 6, 7, 8, 9, 13, 4 | cantnfp1lem2 8459 |
. . 3
⊢ (𝜑 → dom 𝑂 = suc ∪ dom
𝑂) |
15 | 14 | fveq2d 6107 |
. 2
⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom
𝑂)) |
16 | 1, 2, 3, 4, 10 | cantnfcl 8447 |
. . . . . . 7
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝑂 ∈ ω)) |
17 | 16 | simprd 478 |
. . . . . 6
⊢ (𝜑 → dom 𝑂 ∈ ω) |
18 | 14, 17 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω) |
19 | | peano2b 6973 |
. . . . 5
⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω) |
20 | 18, 19 | sylibr 223 |
. . . 4
⊢ (𝜑 → ∪ dom 𝑂 ∈ ω) |
21 | 1, 2, 3, 4, 10, 11 | cantnfsuc 8450 |
. . . 4
⊢ ((𝜑 ∧ ∪ dom 𝑂 ∈ ω) → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑𝑜 (𝑂‘∪ dom 𝑂)) ·𝑜 (𝐹‘(𝑂‘∪ dom
𝑂))) +𝑜
(𝐻‘∪ dom 𝑂))) |
22 | 20, 21 | mpdan 699 |
. . 3
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑𝑜 (𝑂‘∪ dom 𝑂)) ·𝑜 (𝐹‘(𝑂‘∪ dom
𝑂))) +𝑜
(𝐻‘∪ dom 𝑂))) |
23 | | suppssdm 7195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 supp ∅) ⊆ dom 𝐹 |
24 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → 𝑌 ∈ 𝐴) |
25 | 1, 2, 3 | cantnfs 8446 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
26 | 5, 25 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
27 | 26 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
28 | 27 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → (𝐺‘𝑡) ∈ 𝐴) |
29 | 24, 28 | ifcld 4081 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐵) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) ∈ 𝐴) |
30 | 29, 9 | fmptd 6292 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:𝐵⟶𝐴) |
31 | | fdm 5964 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝐵⟶𝐴 → dom 𝐹 = 𝐵) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝐵) |
33 | 23, 32 | syl5sseq 3616 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹 supp ∅) ⊆ 𝐵) |
34 | 3, 33 | ssexd 4733 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹 supp ∅) ∈ V) |
35 | 16 | simpld 474 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → E We (𝐹 supp ∅)) |
36 | 4 | oiiso 8325 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 supp ∅) ∈ V ∧ E
We (𝐹 supp ∅)) →
𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅))) |
37 | 34, 35, 36 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅))) |
38 | | isof1o 6473 |
. . . . . . . . . . . . . 14
⊢ (𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅)) |
39 | 37, 38 | syl 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 𝑂) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → ◡𝑂:(𝐹 supp ∅)⟶dom 𝑂) |
43 | | iftrue 4042 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑋 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = 𝑌) |
44 | 43, 9 | fvmptg 6189 |
. . . . . . . . . . . . . . 15
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝐹‘𝑋) = 𝑌) |
45 | 6, 7, 44 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹‘𝑋) = 𝑌) |
46 | | onelon 5665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ On) |
47 | 2, 7, 46 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑌 ∈ On) |
48 | | on0eln0 5697 |
. . . . . . . . . . . . . . . 16
⊢ (𝑌 ∈ On → (∅
∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
50 | 13, 49 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ≠ ∅) |
51 | 45, 50 | eqnetrd 2849 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹‘𝑋) ≠ ∅) |
52 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝐵⟶𝐴 → 𝐹 Fn 𝐵) |
53 | 30, 52 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 Fn 𝐵) |
54 | | 0ex 4718 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
55 | 54 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈
V) |
56 | | elsuppfn 7190 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) |
57 | 53, 3, 55, 56 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 ∈ (𝐹 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ≠ ∅))) |
58 | 6, 51, 57 | mpbir2and 959 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ (𝐹 supp ∅)) |
59 | 42, 58 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂) |
60 | | elssuni 4403 |
. . . . . . . . . . 11
⊢ ((◡𝑂‘𝑋) ∈ dom 𝑂 → (◡𝑂‘𝑋) ⊆ ∪ dom
𝑂) |
61 | 59, 60 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝑂‘𝑋) ⊆ ∪ dom
𝑂) |
62 | 4 | oicl 8317 |
. . . . . . . . . . . 12
⊢ Ord dom
𝑂 |
63 | | ordelon 5664 |
. . . . . . . . . . . 12
⊢ ((Ord dom
𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On) |
64 | 62, 59, 63 | sylancr 694 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On) |
65 | | nnon 6963 |
. . . . . . . . . . . 12
⊢ (∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ On) |
66 | 20, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ dom 𝑂 ∈ On) |
67 | | ontri1 5674 |
. . . . . . . . . . 11
⊢ (((◡𝑂‘𝑋) ∈ On ∧ ∪ dom 𝑂 ∈ On) → ((◡𝑂‘𝑋) ⊆ ∪ dom
𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))) |
68 | 64, 66, 67 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((◡𝑂‘𝑋) ⊆ ∪ dom
𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))) |
69 | 61, 68 | mpbid 221 |
. . . . . . . . 9
⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)) |
70 | | sucidg 5720 |
. . . . . . . . . . . . . 14
⊢ (∪ dom 𝑂 ∈ ω → ∪ dom 𝑂 ∈ suc ∪ dom
𝑂) |
71 | 20, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ dom 𝑂 ∈ suc ∪ dom
𝑂) |
72 | 71, 14 | eleqtrrd 2691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂) |
73 | | isorel 6476 |
. . . . . . . . . . . 12
⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom
𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) E (𝑂‘(◡𝑂‘𝑋)))) |
74 | 37, 72, 59, 73 | syl12anc 1316 |
. . . . . . . . . . 11
⊢ (𝜑 → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) E (𝑂‘(◡𝑂‘𝑋)))) |
75 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (◡𝑂‘𝑋) ∈ V |
76 | 75 | epelc 4951 |
. . . . . . . . . . 11
⊢ (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ ∪ dom
𝑂 ∈ (◡𝑂‘𝑋)) |
77 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V |
78 | 77 | epelc 4951 |
. . . . . . . . . . 11
⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋))) |
79 | 74, 76, 78 | 3bitr3g 301 |
. . . . . . . . . 10
⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)))) |
80 | | f1ocnvfv2 6433 |
. . . . . . . . . . . 12
⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) ∧ 𝑋 ∈ (𝐹 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
81 | 39, 58, 80 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋) |
82 | 81 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom
𝑂) ∈ 𝑋)) |
83 | 79, 82 | bitrd 267 |
. . . . . . . . 9
⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom
𝑂) ∈ 𝑋)) |
84 | 69, 83 | mtbid 313 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑂‘∪ dom
𝑂) ∈ 𝑋) |
85 | 8 | sseld 3567 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) → (𝑂‘∪ dom 𝑂) ∈ 𝑋)) |
86 | | onss 6882 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
87 | 3, 86 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆ On) |
88 | 33, 87 | sstrd 3578 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 supp ∅) ⊆ On) |
89 | 4 | oif 8318 |
. . . . . . . . . . . . . . . 16
⊢ 𝑂:dom 𝑂⟶(𝐹 supp ∅) |
90 | 89 | ffvelrni 6266 |
. . . . . . . . . . . . . . 15
⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom
𝑂) ∈ (𝐹 supp ∅)) |
91 | 72, 90 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈ (𝐹 supp ∅)) |
92 | 88, 91 | sseldd 3569 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈
On) |
93 | | eloni 5650 |
. . . . . . . . . . . . 13
⊢ ((𝑂‘∪ dom 𝑂) ∈ On → Ord (𝑂‘∪ dom
𝑂)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord (𝑂‘∪ dom
𝑂)) |
95 | | ordn2lp 5660 |
. . . . . . . . . . . 12
⊢ (Ord
(𝑂‘∪ dom 𝑂) → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
96 | 94, 95 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
97 | | imnan 437 |
. . . . . . . . . . 11
⊢ (((𝑂‘∪ dom 𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) ↔ ¬ ((𝑂‘∪ dom 𝑂) ∈ 𝑋 ∧ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
98 | 96, 97 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ 𝑋 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
99 | 85, 98 | syld 46 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) → ¬
𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
100 | | onelon 5665 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On) |
101 | 3, 6, 100 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈ On) |
102 | | eloni 5650 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ On → Ord 𝑋) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → Ord 𝑋) |
104 | | ordirr 5658 |
. . . . . . . . . . 11
⊢ (Ord
𝑋 → ¬ 𝑋 ∈ 𝑋) |
105 | 103, 104 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑋 ∈ 𝑋) |
106 | | elsni 4142 |
. . . . . . . . . . . 12
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (𝑂‘∪ dom
𝑂) = 𝑋) |
107 | 106 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (𝑋 ∈ (𝑂‘∪ dom
𝑂) ↔ 𝑋 ∈ 𝑋)) |
108 | 107 | notbid 307 |
. . . . . . . . . 10
⊢ ((𝑂‘∪ dom 𝑂) ∈ {𝑋} → (¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂) ↔ ¬ 𝑋 ∈ 𝑋)) |
109 | 105, 108 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ {𝑋} → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
110 | | eldifi 3694 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ 𝐵) |
111 | 110 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑘 ∈ 𝐵) |
112 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → 𝑌 ∈ 𝐴) |
113 | | fvex 6113 |
. . . . . . . . . . . . . . 15
⊢ (𝐺‘𝑘) ∈ V |
114 | | ifexg 4107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐺‘𝑘) ∈ V) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) |
115 | 112, 113,
114 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) |
116 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑘 → (𝑡 = 𝑋 ↔ 𝑘 = 𝑋)) |
117 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝑘 → (𝐺‘𝑡) = (𝐺‘𝑘)) |
118 | 116, 117 | ifbieq2d 4061 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 = 𝑘 → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
119 | 118, 9 | fvmptg 6189 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ 𝐵 ∧ if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
120 | 111, 115,
119 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
121 | | eldifn 3695 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
122 | 121 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
123 | | velsn 4141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑋} ↔ 𝑘 = 𝑋) |
124 | | elun2 3743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ {𝑋} → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
125 | 123, 124 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑋 → 𝑘 ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
126 | 122, 125 | nsyl 134 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → ¬ 𝑘 = 𝑋) |
127 | 126 | iffalsed 4047 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = (𝐺‘𝑘)) |
128 | | ssun1 3738 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) |
129 | | sscon 3706 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋}) → (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅))) |
130 | 128, 129 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) ⊆ (𝐵 ∖ (𝐺 supp ∅)) |
131 | 130 | sseli 3564 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋})) → 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) |
132 | | ssid 3587 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 supp ∅) ⊆ (𝐺 supp ∅) |
133 | 132 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅)) |
134 | 27, 133, 3, 13 | suppssr 7213 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑘) = ∅) |
135 | 131, 134 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐺‘𝑘) = ∅) |
136 | 120, 127,
135 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ ((𝐺 supp ∅) ∪ {𝑋}))) → (𝐹‘𝑘) = ∅) |
137 | 30, 136 | suppss 7212 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ((𝐺 supp ∅) ∪ {𝑋})) |
138 | 137, 91 | sseldd 3569 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋})) |
139 | | elun 3715 |
. . . . . . . . . 10
⊢ ((𝑂‘∪ dom 𝑂) ∈ ((𝐺 supp ∅) ∪ {𝑋}) ↔ ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂‘∪ dom 𝑂) ∈ {𝑋})) |
140 | 138, 139 | sylib 207 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) ∈ (𝐺 supp ∅) ∨ (𝑂‘∪ dom 𝑂) ∈ {𝑋})) |
141 | 99, 109, 140 | mpjaod 395 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) |
142 | | ioran 510 |
. . . . . . . 8
⊢ (¬
((𝑂‘∪ dom 𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)) ↔ (¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋 ∧ ¬ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
143 | 84, 141, 142 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂))) |
144 | | ordtri3 5676 |
. . . . . . . 8
⊢ ((Ord
(𝑂‘∪ dom 𝑂) ∧ Ord 𝑋) → ((𝑂‘∪ dom
𝑂) = 𝑋 ↔ ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)))) |
145 | 94, 103, 144 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝑂‘∪ dom
𝑂) = 𝑋 ↔ ¬ ((𝑂‘∪ dom
𝑂) ∈ 𝑋 ∨ 𝑋 ∈ (𝑂‘∪ dom
𝑂)))) |
146 | 143, 145 | mpbird 246 |
. . . . . 6
⊢ (𝜑 → (𝑂‘∪ dom
𝑂) = 𝑋) |
147 | 146 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → (𝐴 ↑𝑜 (𝑂‘∪ dom 𝑂)) = (𝐴 ↑𝑜 𝑋)) |
148 | 146 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (𝐹‘(𝑂‘∪ dom
𝑂)) = (𝐹‘𝑋)) |
149 | 148, 45 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (𝐹‘(𝑂‘∪ dom
𝑂)) = 𝑌) |
150 | 147, 149 | oveq12d 6567 |
. . . 4
⊢ (𝜑 → ((𝐴 ↑𝑜 (𝑂‘∪ dom 𝑂)) ·𝑜 (𝐹‘(𝑂‘∪ dom
𝑂))) = ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌)) |
151 | | nnord 6965 |
. . . . . . . . 9
⊢ (∪ dom 𝑂 ∈ ω → Ord ∪ dom 𝑂) |
152 | 20, 151 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Ord ∪ dom 𝑂) |
153 | | sssucid 5719 |
. . . . . . . . . 10
⊢ ∪ dom 𝑂 ⊆ suc ∪
dom 𝑂 |
154 | 153, 14 | syl5sseqr 3617 |
. . . . . . . . 9
⊢ (𝜑 → ∪ dom 𝑂 ⊆ dom 𝑂) |
155 | | f1ofo 6057 |
. . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) → 𝑂:dom 𝑂–onto→(𝐹 supp ∅)) |
156 | 39, 155 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑂:dom 𝑂–onto→(𝐹 supp ∅)) |
157 | | foima 6033 |
. . . . . . . . . . . 12
⊢ (𝑂:dom 𝑂–onto→(𝐹 supp ∅) → (𝑂 “ dom 𝑂) = (𝐹 supp ∅)) |
158 | 156, 157 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ dom 𝑂) = (𝐹 supp ∅)) |
159 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝑂:dom 𝑂⟶(𝐹 supp ∅) → 𝑂 Fn dom 𝑂) |
160 | 89, 159 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ 𝑂 Fn dom 𝑂 |
161 | | fnsnfv 6168 |
. . . . . . . . . . . . 13
⊢ ((𝑂 Fn dom 𝑂 ∧ ∪ dom
𝑂 ∈ dom 𝑂) → {(𝑂‘∪ dom
𝑂)} = (𝑂 “ {∪ dom
𝑂})) |
162 | 160, 72, 161 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → {(𝑂‘∪ dom
𝑂)} = (𝑂 “ {∪ dom
𝑂})) |
163 | 146 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ (𝜑 → {(𝑂‘∪ dom
𝑂)} = {𝑋}) |
164 | 162, 163 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ {∪ dom
𝑂}) = {𝑋}) |
165 | 158, 164 | difeq12d 3691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂})) = ((𝐹 supp ∅) ∖ {𝑋})) |
166 | | ordirr 5658 |
. . . . . . . . . . . . . . . . 17
⊢ (Ord
∪ dom 𝑂 → ¬ ∪
dom 𝑂 ∈ ∪ dom 𝑂) |
167 | 152, 166 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ ∪ dom
𝑂) |
168 | | disjsn 4192 |
. . . . . . . . . . . . . . . 16
⊢ ((∪ dom 𝑂 ∩ {∪ dom
𝑂}) = ∅ ↔ ¬
∪ dom 𝑂 ∈ ∪ dom
𝑂) |
169 | 167, 168 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∪ dom 𝑂 ∩ {∪ dom
𝑂}) =
∅) |
170 | | disj3 3973 |
. . . . . . . . . . . . . . 15
⊢ ((∪ dom 𝑂 ∩ {∪ dom
𝑂}) = ∅ ↔ ∪ dom 𝑂 = (∪ dom 𝑂 ∖ {∪ dom 𝑂})) |
171 | 169, 170 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ dom 𝑂 = (∪ dom 𝑂 ∖ {∪ dom 𝑂})) |
172 | | difun2 4000 |
. . . . . . . . . . . . . 14
⊢ ((∪ dom 𝑂 ∪ {∪ dom
𝑂}) ∖ {∪ dom 𝑂}) = (∪ dom 𝑂 ∖ {∪ dom 𝑂}) |
173 | 171, 172 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ dom 𝑂 = ((∪ dom 𝑂 ∪ {∪ dom 𝑂}) ∖ {∪ dom
𝑂})) |
174 | | df-suc 5646 |
. . . . . . . . . . . . . . 15
⊢ suc ∪ dom 𝑂 = (∪ dom 𝑂 ∪ {∪ dom 𝑂}) |
175 | 14, 174 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑂 = (∪ dom 𝑂 ∪ {∪ dom 𝑂})) |
176 | 175 | difeq1d 3689 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (dom 𝑂 ∖ {∪ dom
𝑂}) = ((∪ dom 𝑂 ∪ {∪ dom
𝑂}) ∖ {∪ dom 𝑂})) |
177 | 173, 176 | eqtr4d 2647 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∪ dom 𝑂 = (dom 𝑂 ∖ {∪ dom
𝑂})) |
178 | 177 | imaeq2d 5385 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ ∪ dom
𝑂) = (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂}))) |
179 | | dff1o3 6056 |
. . . . . . . . . . . . 13
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) ↔ (𝑂:dom 𝑂–onto→(𝐹 supp ∅) ∧ Fun ◡𝑂)) |
180 | 179 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑂:dom 𝑂–1-1-onto→(𝐹 supp ∅) → Fun ◡𝑂) |
181 | | imadif 5887 |
. . . . . . . . . . . 12
⊢ (Fun
◡𝑂 → (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) |
182 | 39, 180, 181 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑂 “ (dom 𝑂 ∖ {∪ dom
𝑂})) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) |
183 | 178, 182 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑂 “ ∪ dom
𝑂) = ((𝑂 “ dom 𝑂) ∖ (𝑂 “ {∪ dom
𝑂}))) |
184 | 8, 105 | ssneldd 3571 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ 𝑋 ∈ (𝐺 supp ∅)) |
185 | | disjsn 4192 |
. . . . . . . . . . . . 13
⊢ (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ (𝐺 supp ∅)) |
186 | 184, 185 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺 supp ∅) ∩ {𝑋}) = ∅) |
187 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺‘𝑋) ∈ V |
188 | | dif1o 7467 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
↔ ((𝐺‘𝑋) ∈ V ∧ (𝐺‘𝑋) ≠ ∅)) |
189 | 187, 188 | mpbiran 955 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
↔ (𝐺‘𝑋) ≠ ∅) |
190 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐺:𝐵⟶𝐴 → 𝐺 Fn 𝐵) |
191 | 27, 190 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝐺 Fn 𝐵) |
192 | | elsuppfn 7190 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) |
193 | 191, 3, 55, 192 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅))) |
194 | 189 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
↔ (𝐺‘𝑋) ≠
∅)) |
195 | 194 | bicomd 212 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ ↔ (𝐺‘𝑋) ∈ (V ∖
1𝑜))) |
196 | 195 | anbi2d 736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ≠ ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1𝑜)))) |
197 | 193, 196 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) ↔ (𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖
1𝑜)))) |
198 | 8 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑋 ∈ (𝐺 supp ∅) → 𝑋 ∈ 𝑋)) |
199 | 197, 198 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑋 ∈ 𝐵 ∧ (𝐺‘𝑋) ∈ (V ∖ 1𝑜))
→ 𝑋 ∈ 𝑋)) |
200 | 6, 199 | mpand 707 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺‘𝑋) ∈ (V ∖ 1𝑜)
→ 𝑋 ∈ 𝑋)) |
201 | 189, 200 | syl5bir 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺‘𝑋) ≠ ∅ → 𝑋 ∈ 𝑋)) |
202 | 201 | necon1bd 2800 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (¬ 𝑋 ∈ 𝑋 → (𝐺‘𝑋) = ∅)) |
203 | 105, 202 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺‘𝑋) = ∅) |
204 | 203 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺‘𝑋) = ∅) |
205 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑋 → (𝐺‘𝑘) = (𝐺‘𝑋)) |
206 | 205 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑋 → ((𝐺‘𝑘) = ∅ ↔ (𝐺‘𝑋) = ∅)) |
207 | 204, 206 | syl5ibrcom 236 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝑘 = 𝑋 → (𝐺‘𝑘) = ∅)) |
208 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅)) → 𝑘 ∈ 𝐵) |
209 | 208 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑘 ∈ 𝐵) |
210 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → 𝑌 ∈ 𝐴) |
211 | 210, 113,
114 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) ∈ V) |
212 | 209, 211,
119 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑘) = if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘))) |
213 | | ssid 3587 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 supp ∅) ⊆ (𝐹 supp ∅) |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅)) |
215 | 30, 214, 3, 13 | suppssr 7213 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑘) = ∅) |
216 | 212, 215 | eqtr3d 2646 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = ∅) |
217 | | iffalse 4045 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑘 = 𝑋 → if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = (𝐺‘𝑘)) |
218 | 217 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑘 = 𝑋 → (if(𝑘 = 𝑋, 𝑌, (𝐺‘𝑘)) = ∅ ↔ (𝐺‘𝑘) = ∅)) |
219 | 216, 218 | syl5ibcom 234 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (¬ 𝑘 = 𝑋 → (𝐺‘𝑘) = ∅)) |
220 | 207, 219 | pm2.61d 169 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐺‘𝑘) = ∅) |
221 | 27, 220 | suppss 7212 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐹 supp ∅)) |
222 | | reldisj 3972 |
. . . . . . . . . . . . 13
⊢ ((𝐺 supp ∅) ⊆ (𝐹 supp ∅) → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))) |
223 | 221, 222 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐺 supp ∅) ∩ {𝑋}) = ∅ ↔ (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋}))) |
224 | 186, 223 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐺 supp ∅) ⊆ ((𝐹 supp ∅) ∖ {𝑋})) |
225 | | uncom 3719 |
. . . . . . . . . . . . 13
⊢ ((𝐺 supp ∅) ∪ {𝑋}) = ({𝑋} ∪ (𝐺 supp ∅)) |
226 | 137, 225 | syl6sseq 3614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅))) |
227 | | ssundif 4004 |
. . . . . . . . . . . 12
⊢ ((𝐹 supp ∅) ⊆ ({𝑋} ∪ (𝐺 supp ∅)) ↔ ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅)) |
228 | 226, 227 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 supp ∅) ∖ {𝑋}) ⊆ (𝐺 supp ∅)) |
229 | 224, 228 | eqssd 3585 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 supp ∅) = ((𝐹 supp ∅) ∖ {𝑋})) |
230 | 165, 183,
229 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺 supp ∅) = (𝑂 “ ∪ dom
𝑂)) |
231 | | isores3 6485 |
. . . . . . . . 9
⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐹 supp ∅)) ∧ ∪ dom 𝑂 ⊆ dom 𝑂 ∧ (𝐺 supp ∅) = (𝑂 “ ∪ dom
𝑂)) → (𝑂 ↾ ∪ dom 𝑂) Isom E , E (∪
dom 𝑂, (𝐺 supp ∅))) |
232 | 37, 154, 230, 231 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) |
233 | | cantnfp1.k |
. . . . . . . . . . 11
⊢ 𝐾 = OrdIso( E , (𝐺 supp ∅)) |
234 | 1, 2, 3, 233, 5 | cantnfcl 8447 |
. . . . . . . . . 10
⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝐾 ∈ ω)) |
235 | 234 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → E We (𝐺 supp ∅)) |
236 | | epse 5021 |
. . . . . . . . 9
⊢ E Se
(𝐺 supp
∅) |
237 | 233 | oieu 8327 |
. . . . . . . . 9
⊢ (( E We
(𝐺 supp ∅) ∧ E Se
(𝐺 supp ∅)) →
((Ord ∪ dom 𝑂 ∧ (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) ↔ (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾))) |
238 | 235, 236,
237 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → ((Ord ∪ dom 𝑂 ∧ (𝑂 ↾ ∪ dom
𝑂) Isom E , E (∪ dom 𝑂, (𝐺 supp ∅))) ↔ (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾))) |
239 | 152, 232,
238 | mpbi2and 958 |
. . . . . . 7
⊢ (𝜑 → (∪ dom 𝑂 = dom 𝐾 ∧ (𝑂 ↾ ∪ dom
𝑂) = 𝐾)) |
240 | 239 | simpld 474 |
. . . . . 6
⊢ (𝜑 → ∪ dom 𝑂 = dom 𝐾) |
241 | 240 | fveq2d 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
↦ (((𝐴
↑𝑜 (𝐾‘𝑘)) ·𝑜 (𝐺‘(𝐾‘𝑘))) +𝑜 𝑧)), ∅) |
246 | 245 | seqom0g 7438 |
. . . . . . . . . . . . 13
⊢ (∅
∈ V → (𝑀‘∅) = ∅) |
247 | 54, 246 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑀‘∅) =
∅ |
248 | 244, 247 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (𝑀‘𝑥) = ∅) |
249 | 243, 248 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘∅) = ∅)) |
250 | 242, 249 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (∅ ∈ dom 𝑂 → (𝐻‘∅) =
∅))) |
251 | 250 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) =
∅)))) |
252 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ dom 𝑂 ↔ 𝑦 ∈ dom 𝑂)) |
253 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝐻‘𝑥) = (𝐻‘𝑦)) |
254 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (𝑀‘𝑥) = (𝑀‘𝑦)) |
255 | 253, 254 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘𝑦) = (𝑀‘𝑦))) |
256 | 252, 255 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)))) |
257 | 256 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))))) |
258 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ dom 𝑂 ↔ suc 𝑦 ∈ dom 𝑂)) |
259 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝐻‘𝑥) = (𝐻‘suc 𝑦)) |
260 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = suc 𝑦 → (𝑀‘𝑥) = (𝑀‘suc 𝑦)) |
261 | 259, 260 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = suc 𝑦 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))) |
262 | 258, 261 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) |
263 | 262 | imbi2d 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
𝑂)) |
267 | 265, 266 | eqeq12d 2625 |
. . . . . . . . . 10
⊢ (𝑥 = ∪
dom 𝑂 → ((𝐻‘𝑥) = (𝑀‘𝑥) ↔ (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))) |
268 | 264, 267 | imbi12d 333 |
. . . . . . . . 9
⊢ (𝑥 = ∪
dom 𝑂 → ((𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥)) ↔ (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)))) |
269 | 268 | imbi2d 329 |
. . . . . . . 8
⊢ (𝑥 = ∪
dom 𝑂 → ((𝜑 → (𝑥 ∈ dom 𝑂 → (𝐻‘𝑥) = (𝑀‘𝑥))) ↔ (𝜑 → (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))))) |
270 | 11 | seqom0g 7438 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝐻‘∅) = ∅) |
271 | 54, 270 | mp1i 13 |
. . . . . . . . 9
⊢ (∅
∈ dom 𝑂 → (𝐻‘∅) =
∅) |
272 | 271 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → (∅ ∈ dom 𝑂 → (𝐻‘∅) = ∅)) |
273 | | nnord 6965 |
. . . . . . . . . . . . . . . 16
⊢ (dom
𝑂 ∈ ω → Ord
dom 𝑂) |
274 | 17, 273 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → Ord dom 𝑂) |
275 | | ordtr 5654 |
. . . . . . . . . . . . . . 15
⊢ (Ord dom
𝑂 → Tr dom 𝑂) |
276 | 274, 275 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Tr dom 𝑂) |
277 | | trsuc 5727 |
. . . . . . . . . . . . . 14
⊢ ((Tr dom
𝑂 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂) |
278 | 276, 277 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝑂) |
279 | 278 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → 𝑦 ∈ dom 𝑂)) |
280 | 279 | imim1d 80 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)))) |
281 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ ((𝐻‘𝑦) = (𝑀‘𝑦) → (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝐻‘𝑦)) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝑀‘𝑦))) |
282 | | elnn 6967 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → 𝑦 ∈ ω) |
283 | 282 | ancoms 468 |
. . . . . . . . . . . . . . . . . 18
⊢ ((dom
𝑂 ∈ ω ∧
𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω) |
284 | 17, 283 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω) |
285 | 278, 284 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ω) |
286 | 1, 2, 3, 4, 10, 11 | cantnfsuc 8450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝐻‘suc 𝑦) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝐻‘𝑦))) |
287 | 285, 286 | syldan 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐻‘suc 𝑦) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝐻‘𝑦))) |
288 | 1, 2, 3, 233, 5, 245 | cantnfsuc 8450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ω) → (𝑀‘suc 𝑦) = (((𝐴 ↑𝑜 (𝐾‘𝑦)) ·𝑜 (𝐺‘(𝐾‘𝑦))) +𝑜 (𝑀‘𝑦))) |
289 | 285, 288 | syldan 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴 ↑𝑜 (𝐾‘𝑦)) ·𝑜 (𝐺‘(𝐾‘𝑦))) +𝑜 (𝑀‘𝑦))) |
290 | 239 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑂 ↾ ∪ dom
𝑂) = 𝐾) |
291 | 290 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝐾‘𝑦)) |
292 | 291 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝐾‘𝑦)) |
293 | 14 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 ↔ suc 𝑦 ∈ suc ∪ dom
𝑂)) |
294 | 293 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → suc 𝑦 ∈ suc ∪ dom
𝑂) |
295 | 152 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → Ord ∪
dom 𝑂) |
296 | | ordsucelsuc 6914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Ord
∪ dom 𝑂 → (𝑦 ∈ ∪ dom
𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂)) |
297 | 295, 296 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑦 ∈ ∪ dom
𝑂 ↔ suc 𝑦 ∈ suc ∪ dom 𝑂)) |
298 | 294, 297 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ ∪ dom
𝑂) |
299 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 ∈ ∪ dom 𝑂 → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝑂‘𝑦)) |
300 | 298, 299 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝑂 ↾ ∪ dom
𝑂)‘𝑦) = (𝑂‘𝑦)) |
301 | 292, 300 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) = (𝑂‘𝑦)) |
302 | 301 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐴 ↑𝑜 (𝐾‘𝑦)) = (𝐴 ↑𝑜 (𝑂‘𝑦))) |
303 | | suppssdm 7195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 |
304 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵) |
305 | 27, 304 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → dom 𝐺 = 𝐵) |
306 | 303, 305 | syl5sseq 3616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) |
307 | 306 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺 supp ∅) ⊆ 𝐵) |
308 | 240 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ∪ dom
𝑂 = dom 𝐾) |
309 | 298, 308 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑦 ∈ dom 𝐾) |
310 | 233 | oif 8318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐾:dom 𝐾⟶(𝐺 supp ∅) |
311 | 310 | ffvelrni 6266 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ∈ dom 𝐾 → (𝐾‘𝑦) ∈ (𝐺 supp ∅)) |
312 | 309, 311 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) ∈ (𝐺 supp ∅)) |
313 | 307, 312 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐾‘𝑦) ∈ 𝐵) |
314 | 7 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → 𝑌 ∈ 𝐴) |
315 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺‘(𝐾‘𝑦)) ∈ V |
316 | | ifexg 4107 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐺‘(𝐾‘𝑦)) ∈ V) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) ∈ V) |
317 | 314, 315,
316 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) ∈ V) |
318 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝐾‘𝑦) → (𝑡 = 𝑋 ↔ (𝐾‘𝑦) = 𝑋)) |
319 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑡 = (𝐾‘𝑦) → (𝐺‘𝑡) = (𝐺‘(𝐾‘𝑦))) |
320 | 318, 319 | ifbieq2d 4061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑡 = (𝐾‘𝑦) → if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡)) = if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦)))) |
321 | 320, 9 | fvmptg 6189 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐾‘𝑦) ∈ 𝐵 ∧ if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) ∈ V) → (𝐹‘(𝐾‘𝑦)) = if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦)))) |
322 | 313, 317,
321 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾‘𝑦)) = if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦)))) |
323 | 301 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐹‘(𝐾‘𝑦)) = (𝐹‘(𝑂‘𝑦))) |
324 | 184 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ 𝑋 ∈ (𝐺 supp ∅)) |
325 | | nelneq 2712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐾‘𝑦) ∈ (𝐺 supp ∅) ∧ ¬ 𝑋 ∈ (𝐺 supp ∅)) → ¬ (𝐾‘𝑦) = 𝑋) |
326 | 312, 324,
325 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ¬ (𝐾‘𝑦) = 𝑋) |
327 | 326 | iffalsed 4047 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → if((𝐾‘𝑦) = 𝑋, 𝑌, (𝐺‘(𝐾‘𝑦))) = (𝐺‘(𝐾‘𝑦))) |
328 | 322, 323,
327 | 3eqtr3rd 2653 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝐺‘(𝐾‘𝑦)) = (𝐹‘(𝑂‘𝑦))) |
329 | 302, 328 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐴 ↑𝑜 (𝐾‘𝑦)) ·𝑜 (𝐺‘(𝐾‘𝑦))) = ((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦)))) |
330 | 329 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (((𝐴 ↑𝑜 (𝐾‘𝑦)) ·𝑜 (𝐺‘(𝐾‘𝑦))) +𝑜 (𝑀‘𝑦)) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝑀‘𝑦))) |
331 | 289, 330 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → (𝑀‘suc 𝑦) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝑀‘𝑦))) |
332 | 287, 331 | eqeq12d 2625 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘suc 𝑦) = (𝑀‘suc 𝑦) ↔ (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝐻‘𝑦)) = (((𝐴 ↑𝑜 (𝑂‘𝑦)) ·𝑜 (𝐹‘(𝑂‘𝑦))) +𝑜 (𝑀‘𝑦)))) |
333 | 281, 332 | syl5ibr 235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ suc 𝑦 ∈ dom 𝑂) → ((𝐻‘𝑦) = (𝑀‘𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))) |
334 | 333 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (suc 𝑦 ∈ dom 𝑂 → ((𝐻‘𝑦) = (𝑀‘𝑦) → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) |
335 | 334 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝜑 → ((suc 𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) |
336 | 280, 335 | syld 46 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦)) → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) |
337 | 336 | a2i 14 |
. . . . . . . . 9
⊢ ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦)))) |
338 | 337 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → ((𝜑 → (𝑦 ∈ dom 𝑂 → (𝐻‘𝑦) = (𝑀‘𝑦))) → (𝜑 → (suc 𝑦 ∈ dom 𝑂 → (𝐻‘suc 𝑦) = (𝑀‘suc 𝑦))))) |
339 | 251, 257,
263, 269, 272, 338 | finds 6984 |
. . . . . . 7
⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → (∪ dom
𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)))) |
340 | 20, 339 | mpcom 37 |
. . . . . 6
⊢ (𝜑 → (∪ dom 𝑂 ∈ dom 𝑂 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂))) |
341 | 72, 340 | mpd 15 |
. . . . 5
⊢ (𝜑 → (𝐻‘∪ dom
𝑂) = (𝑀‘∪ dom
𝑂)) |
342 | 1, 2, 3, 233, 5, 245 | cantnfval 8448 |
. . . . 5
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝑀‘dom 𝐾)) |
343 | 241, 341,
342 | 3eqtr4d 2654 |
. . . 4
⊢ (𝜑 → (𝐻‘∪ dom
𝑂) = ((𝐴 CNF 𝐵)‘𝐺)) |
344 | 150, 343 | oveq12d 6567 |
. . 3
⊢ (𝜑 → (((𝐴 ↑𝑜 (𝑂‘∪ dom 𝑂)) ·𝑜 (𝐹‘(𝑂‘∪ dom
𝑂))) +𝑜
(𝐻‘∪ dom 𝑂)) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |
345 | 22, 344 | eqtrd 2644 |
. 2
⊢ (𝜑 → (𝐻‘suc ∪ dom
𝑂) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |
346 | 12, 15, 345 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |