Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . . . 5
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
2 | | cantnfs.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | cantnfs.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ On) |
4 | | cantnf.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
5 | | oemapval.t |
. . . . . . . . . . . . . 14
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
6 | | cantnf.c |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) |
7 | | cantnf.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ⊆ ran (𝐴 CNF 𝐵)) |
8 | | cantnf.e |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈ 𝐶) |
9 | 1, 2, 3, 5, 6, 7, 8 | cantnflem2 8470 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ (On ∖ 2𝑜)
∧ 𝐶 ∈ (On ∖
1𝑜))) |
10 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = 𝑋 |
11 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = 𝑌 |
12 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = 𝑍 |
13 | 10, 11, 12 | 3pm3.2i 1232 |
. . . . . . . . . . . . . 14
⊢ (𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍) |
14 | | cantnf.x |
. . . . . . . . . . . . . . 15
⊢ 𝑋 = ∪
∩ {𝑐 ∈ On ∣ 𝐶 ∈ (𝐴 ↑𝑜 𝑐)} |
15 | | cantnf.p |
. . . . . . . . . . . . . . 15
⊢ 𝑃 = (℩𝑑∃𝑎 ∈ On ∃𝑏 ∈ (𝐴 ↑𝑜 𝑋)(𝑑 = 〈𝑎, 𝑏〉 ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑎) +𝑜
𝑏) = 𝐶)) |
16 | | cantnf.y |
. . . . . . . . . . . . . . 15
⊢ 𝑌 = (1st ‘𝑃) |
17 | | cantnf.z |
. . . . . . . . . . . . . . 15
⊢ 𝑍 = (2nd ‘𝑃) |
18 | 14, 15, 16, 17 | oeeui 7569 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜))
→ (((𝑋 ∈ On ∧
𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
𝑍) = 𝐶) ↔ (𝑋 = 𝑋 ∧ 𝑌 = 𝑌 ∧ 𝑍 = 𝑍))) |
19 | 13, 18 | mpbiri 247 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐶 ∈ (On ∖ 1𝑜))
→ ((𝑋 ∈ On ∧
𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
𝑍) = 𝐶)) |
20 | 9, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) ∧ (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
𝑍) = 𝐶)) |
21 | 20 | simpld 474 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋 ∈ On ∧ 𝑌 ∈ (𝐴 ∖ 1𝑜) ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋))) |
22 | 21 | simp1d 1066 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ On) |
23 | | oecl 7504 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑋 ∈ On) → (𝐴 ↑𝑜
𝑋) ∈
On) |
24 | 2, 22, 23 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ∈ On) |
25 | 21 | simp2d 1067 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ (𝐴 ∖
1𝑜)) |
26 | 25 | eldifad 3552 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ 𝐴) |
27 | | onelon 5665 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ On) |
28 | 2, 26, 27 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ On) |
29 | | dif1o 7467 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (𝐴 ∖ 1𝑜) ↔
(𝑌 ∈ 𝐴 ∧ 𝑌 ≠ ∅)) |
30 | 29 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (𝐴 ∖ 1𝑜) → 𝑌 ≠ ∅) |
31 | 25, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ≠ ∅) |
32 | | on0eln0 5697 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ On → (∅
∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (∅ ∈ 𝑌 ↔ 𝑌 ≠ ∅)) |
34 | 31, 33 | mpbird 246 |
. . . . . . . . 9
⊢ (𝜑 → ∅ ∈ 𝑌) |
35 | | omword1 7540 |
. . . . . . . . 9
⊢ ((((𝐴 ↑𝑜
𝑋) ∈ On ∧ 𝑌 ∈ On) ∧ ∅ ∈
𝑌) → (𝐴 ↑𝑜
𝑋) ⊆ ((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌)) |
36 | 24, 28, 34, 35 | syl21anc 1317 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ⊆ ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌)) |
37 | | omcl 7503 |
. . . . . . . . . . 11
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ 𝑌 ∈ On) → ((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌) ∈ On) |
38 | 24, 28, 37 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) ∈
On) |
39 | 21 | simp3d 1068 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) |
40 | | onelon 5665 |
. . . . . . . . . . 11
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) → 𝑍 ∈ On) |
41 | 24, 39, 40 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑍 ∈ On) |
42 | | oaword1 7519 |
. . . . . . . . . 10
⊢ ((((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌) ∈ On ∧ 𝑍 ∈ On) → ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) ⊆ (((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌) +𝑜 𝑍)) |
43 | 38, 41, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) ⊆ (((𝐴 ↑𝑜
𝑋)
·𝑜 𝑌) +𝑜 𝑍)) |
44 | 20 | simprd 478 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
𝑍) = 𝐶) |
45 | 43, 44 | sseqtrd 3604 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) ⊆ 𝐶) |
46 | 36, 45 | sstrd 3578 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ⊆ 𝐶) |
47 | | oecl 7504 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
48 | 2, 3, 47 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ↑𝑜 𝐵) ∈ On) |
49 | | ontr2 5689 |
. . . . . . . 8
⊢ (((𝐴 ↑𝑜
𝑋) ∈ On ∧ (𝐴 ↑𝑜
𝐵) ∈ On) →
(((𝐴
↑𝑜 𝑋) ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) → (𝐴 ↑𝑜 𝑋) ∈ (𝐴 ↑𝑜 𝐵))) |
50 | 24, 48, 49 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ⊆ 𝐶 ∧ 𝐶 ∈ (𝐴 ↑𝑜 𝐵)) → (𝐴 ↑𝑜 𝑋) ∈ (𝐴 ↑𝑜 𝐵))) |
51 | 46, 6, 50 | mp2and 711 |
. . . . . 6
⊢ (𝜑 → (𝐴 ↑𝑜 𝑋) ∈ (𝐴 ↑𝑜 𝐵)) |
52 | 9 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (On ∖
2𝑜)) |
53 | | oeord 7555 |
. . . . . . 7
⊢ ((𝑋 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝑋 ∈ 𝐵 ↔ (𝐴 ↑𝑜 𝑋) ∈ (𝐴 ↑𝑜 𝐵))) |
54 | 22, 3, 52, 53 | syl3anc 1318 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ (𝐴 ↑𝑜 𝑋) ∈ (𝐴 ↑𝑜 𝐵))) |
55 | 51, 54 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
56 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ On) |
57 | 3 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐵 ∈ On) |
58 | | suppssdm 7195 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 supp ∅) ⊆ dom 𝐺 |
59 | 1, 2, 3 | cantnfs 8446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
60 | 4, 59 | mpbid 221 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
61 | 60 | simpld 474 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
62 | | fdm 5964 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → dom 𝐺 = 𝐵) |
64 | 58, 63 | syl5sseq 3616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵) |
65 | 64 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ 𝐵) |
66 | | onelon 5665 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
67 | 57, 65, 66 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ On) |
68 | | oecl 7504 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (𝐴 ↑𝑜
𝑥) ∈
On) |
69 | 56, 67, 68 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑𝑜 𝑥) ∈ On) |
70 | 61 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐺:𝐵⟶𝐴) |
71 | 70, 65 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ∈ 𝐴) |
72 | | onelon 5665 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑥) ∈ 𝐴) → (𝐺‘𝑥) ∈ On) |
73 | 56, 71, 72 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ∈ On) |
74 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝐵⟶𝐴 → 𝐺 Fn 𝐵) |
75 | 61, 74 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺 Fn 𝐵) |
76 | | 0ex 4718 |
. . . . . . . . . . . . . . 15
⊢ ∅
∈ V |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∅ ∈
V) |
78 | | elsuppfn 7190 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) →
(𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝐺‘𝑥) ≠ ∅))) |
79 | 75, 3, 77, 78 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ (𝐺 supp ∅) ↔ (𝑥 ∈ 𝐵 ∧ (𝐺‘𝑥) ≠ ∅))) |
80 | 79 | simplbda 652 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐺‘𝑥) ≠ ∅) |
81 | | on0eln0 5697 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘𝑥) ∈ On → (∅ ∈ (𝐺‘𝑥) ↔ (𝐺‘𝑥) ≠ ∅)) |
82 | 73, 81 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∅ ∈
(𝐺‘𝑥) ↔ (𝐺‘𝑥) ≠ ∅)) |
83 | 80, 82 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∅ ∈ (𝐺‘𝑥)) |
84 | | omword1 7540 |
. . . . . . . . . . 11
⊢ ((((𝐴 ↑𝑜
𝑥) ∈ On ∧ (𝐺‘𝑥) ∈ On) ∧ ∅ ∈ (𝐺‘𝑥)) → (𝐴 ↑𝑜 𝑥) ⊆ ((𝐴 ↑𝑜 𝑥) ·𝑜
(𝐺‘𝑥))) |
85 | 69, 73, 83, 84 | syl21anc 1317 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑𝑜 𝑥) ⊆ ((𝐴 ↑𝑜 𝑥) ·𝑜
(𝐺‘𝑥))) |
86 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ OrdIso( E
, (𝐺 supp ∅)) =
OrdIso( E , (𝐺 supp
∅)) |
87 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐺 ∈ 𝑆) |
88 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐺 supp
∅))‘𝑘))
·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝐺 supp
∅))‘𝑘))
·𝑜 (𝐺‘(OrdIso( E , (𝐺 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
89 | 1, 56, 57, 86, 87, 88, 65 | cantnfle 8451 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 ↑𝑜 𝑥) ·𝑜
(𝐺‘𝑥)) ⊆ ((𝐴 CNF 𝐵)‘𝐺)) |
90 | | cantnf.v |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍) |
91 | 90 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 CNF 𝐵)‘𝐺) = 𝑍) |
92 | 89, 91 | sseqtrd 3604 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝐴 ↑𝑜 𝑥) ·𝑜
(𝐺‘𝑥)) ⊆ 𝑍) |
93 | 85, 92 | sstrd 3578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑𝑜 𝑥) ⊆ 𝑍) |
94 | 39 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) |
95 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑𝑜 𝑋) ∈ On) |
96 | | ontr2 5689 |
. . . . . . . . . 10
⊢ (((𝐴 ↑𝑜
𝑥) ∈ On ∧ (𝐴 ↑𝑜
𝑋) ∈ On) →
(((𝐴
↑𝑜 𝑥) ⊆ 𝑍 ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) → (𝐴 ↑𝑜 𝑥) ∈ (𝐴 ↑𝑜 𝑋))) |
97 | 69, 95, 96 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (((𝐴 ↑𝑜 𝑥) ⊆ 𝑍 ∧ 𝑍 ∈ (𝐴 ↑𝑜 𝑋)) → (𝐴 ↑𝑜 𝑥) ∈ (𝐴 ↑𝑜 𝑋))) |
98 | 93, 94, 97 | mp2and 711 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝐴 ↑𝑜 𝑥) ∈ (𝐴 ↑𝑜 𝑋)) |
99 | 22 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑋 ∈ On) |
100 | 52 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝐴 ∈ (On ∖
2𝑜)) |
101 | | oeord 7555 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑋 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝑥 ∈ 𝑋 ↔ (𝐴 ↑𝑜 𝑥) ∈ (𝐴 ↑𝑜 𝑋))) |
102 | 67, 99, 100, 101 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑥 ∈ 𝑋 ↔ (𝐴 ↑𝑜 𝑥) ∈ (𝐴 ↑𝑜 𝑋))) |
103 | 98, 102 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑥 ∈ 𝑋) |
104 | 103 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐺 supp ∅) → 𝑥 ∈ 𝑋)) |
105 | 104 | ssrdv 3574 |
. . . . 5
⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝑋) |
106 | | cantnf.f |
. . . . 5
⊢ 𝐹 = (𝑡 ∈ 𝐵 ↦ if(𝑡 = 𝑋, 𝑌, (𝐺‘𝑡))) |
107 | 1, 2, 3, 4, 55, 26, 105, 106 | cantnfp1 8461 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)))) |
108 | 107 | simprd 478 |
. . 3
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺))) |
109 | 90 | oveq2d 6565 |
. . 3
⊢ (𝜑 → (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
((𝐴 CNF 𝐵)‘𝐺)) = (((𝐴 ↑𝑜 𝑋) ·𝑜
𝑌) +𝑜
𝑍)) |
110 | 108, 109,
44 | 3eqtrd 2648 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = 𝐶) |
111 | 1, 2, 3 | cantnff 8454 |
. . . 4
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |
112 | | ffn 5958 |
. . . 4
⊢ ((𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵) → (𝐴 CNF 𝐵) Fn 𝑆) |
113 | 111, 112 | syl 17 |
. . 3
⊢ (𝜑 → (𝐴 CNF 𝐵) Fn 𝑆) |
114 | 107 | simpld 474 |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
115 | | fnfvelrn 6264 |
. . 3
⊢ (((𝐴 CNF 𝐵) Fn 𝑆 ∧ 𝐹 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵)) |
116 | 113, 114,
115 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ran (𝐴 CNF 𝐵)) |
117 | 110, 116 | eqeltrrd 2689 |
1
⊢ (𝜑 → 𝐶 ∈ ran (𝐴 CNF 𝐵)) |