Step | Hyp | Ref
| Expression |
1 | | limccnp2.h |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) |
2 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ∪ 𝐽 =
∪ 𝐽 |
3 | 2 | cnprcl 21049 |
. . . . . . . . . . 11
⊢ (𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉) → 〈𝐶, 𝐷〉 ∈ ∪
𝐽) |
4 | 1, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ ∪
𝐽) |
5 | | limccnp2.j |
. . . . . . . . . . . 12
⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) |
6 | | limccnp2.k |
. . . . . . . . . . . . . . 15
⊢ 𝐾 =
(TopOpen‘ℂfld) |
7 | 6 | cnfldtopon 22586 |
. . . . . . . . . . . . . 14
⊢ 𝐾 ∈
(TopOn‘ℂ) |
8 | | txtopon 21394 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐾 ∈
(TopOn‘ℂ)) → (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ ×
ℂ))) |
9 | 7, 7, 8 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ
× ℂ)) |
10 | | limccnp2.x |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
11 | | limccnp2.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
12 | | xpss12 5225 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ)) |
13 | 10, 11, 12 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ)) |
14 | | resttopon 20965 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ
× ℂ)) ∧ (𝑋
× 𝑌) ⊆ (ℂ
× ℂ)) → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ (TopOn‘(𝑋 × 𝑌))) |
15 | 9, 13, 14 | sylancr 695 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ (TopOn‘(𝑋 × 𝑌))) |
16 | 5, 15 | syl5eqel 2705 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(𝑋 × 𝑌))) |
17 | | toponuni 20719 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ 𝐽) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝐽) |
19 | 4, 18 | eleqtrrd 2704 |
. . . . . . . . 9
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
20 | | opelxp 5146 |
. . . . . . . . 9
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) ↔ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) |
21 | 19, 20 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) |
22 | 21 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
23 | 22 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ 𝑥 = 𝐵) → 𝐶 ∈ 𝑋) |
24 | | simpll 790 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝜑) |
25 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → 𝑥 ∈ (𝐴 ∪ {𝐵})) |
26 | | elun 3753 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
27 | 25, 26 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
28 | 27 | ord 392 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (¬ 𝑥 ∈ 𝐴 → 𝑥 ∈ {𝐵})) |
29 | | elsni 4194 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
30 | 28, 29 | syl6 35 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (¬ 𝑥 ∈ 𝐴 → 𝑥 = 𝐵)) |
31 | 30 | con1d 139 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (¬ 𝑥 = 𝐵 → 𝑥 ∈ 𝐴)) |
32 | 31 | imp 445 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ 𝐴) |
33 | | limccnp2.r |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋) |
34 | 24, 32, 33 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑅 ∈ 𝑋) |
35 | 23, 34 | ifclda 4120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → if(𝑥 = 𝐵, 𝐶, 𝑅) ∈ 𝑋) |
36 | 21 | simprd 479 |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
37 | 36 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ 𝑥 = 𝐵) → 𝐷 ∈ 𝑌) |
38 | | limccnp2.s |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌) |
39 | 24, 32, 38 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑆 ∈ 𝑌) |
40 | 37, 39 | ifclda 4120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → if(𝑥 = 𝐵, 𝐷, 𝑆) ∈ 𝑌) |
41 | | opelxpi 5148 |
. . . . 5
⊢
((if(𝑥 = 𝐵, 𝐶, 𝑅) ∈ 𝑋 ∧ if(𝑥 = 𝐵, 𝐷, 𝑆) ∈ 𝑌) → 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉 ∈ (𝑋 × 𝑌)) |
42 | 35, 40, 41 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉 ∈ (𝑋 × 𝑌)) |
43 | | eqidd 2623 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)) |
44 | 7 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℂ)) |
45 | | cnpf2 21054 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
46 | 16, 44, 1, 45 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
47 | 46 | feqmptd 6249 |
. . . 4
⊢ (𝜑 → 𝐻 = (𝑦 ∈ (𝑋 × 𝑌) ↦ (𝐻‘𝑦))) |
48 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉 → (𝐻‘𝑦) = (𝐻‘〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)) |
49 | | df-ov 6653 |
. . . . . 6
⊢ (if(𝑥 = 𝐵, 𝐶, 𝑅)𝐻if(𝑥 = 𝐵, 𝐷, 𝑆)) = (𝐻‘〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) |
50 | | ovif12 6739 |
. . . . . 6
⊢ (if(𝑥 = 𝐵, 𝐶, 𝑅)𝐻if(𝑥 = 𝐵, 𝐷, 𝑆)) = if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆)) |
51 | 49, 50 | eqtr3i 2646 |
. . . . 5
⊢ (𝐻‘〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) = if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆)) |
52 | 48, 51 | syl6eq 2672 |
. . . 4
⊢ (𝑦 = 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉 → (𝐻‘𝑦) = if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆))) |
53 | 42, 43, 47, 52 | fmptco 6396 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆)))) |
54 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
55 | 54, 33 | dmmptd 6024 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴) |
56 | | limccnp2.c |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) |
57 | | limcrcl 23638 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅):dom (𝑥 ∈ 𝐴 ↦ 𝑅)⟶ℂ ∧ dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅):dom (𝑥 ∈ 𝐴 ↦ 𝑅)⟶ℂ ∧ dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
59 | 58 | simp2d 1074 |
. . . . . . . . . 10
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ) |
60 | 55, 59 | eqsstr3d 3640 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
61 | 58 | simp3d 1075 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
62 | 61 | snssd 4340 |
. . . . . . . . 9
⊢ (𝜑 → {𝐵} ⊆ ℂ) |
63 | 60, 62 | unssd 3789 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∪ {𝐵}) ⊆ ℂ) |
64 | | resttopon 20965 |
. . . . . . . 8
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) →
(𝐾 ↾t
(𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
65 | 7, 63, 64 | sylancr 695 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
66 | | ssun2 3777 |
. . . . . . . 8
⊢ {𝐵} ⊆ (𝐴 ∪ {𝐵}) |
67 | | snssg 4327 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
68 | 61, 67 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
69 | 66, 68 | mpbiri 248 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
70 | 10 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ⊆ ℂ) |
71 | 70, 33 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
72 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝐾 ↾t (𝐴 ∪ {𝐵})) = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
73 | 60, 61, 71, 72, 6 | limcmpt 23647 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, 𝑅)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
74 | 56, 73 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, 𝑅)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
75 | | limccnp2.d |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) |
76 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ⊆ ℂ) |
77 | 76, 38 | sseldd 3604 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ ℂ) |
78 | 60, 61, 77, 72, 6 | limcmpt 23647 |
. . . . . . . 8
⊢ (𝜑 → (𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐷, 𝑆)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
79 | 75, 78 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐷, 𝑆)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
80 | 65, 44, 44, 69, 74, 79 | txcnp 21423 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ×t 𝐾))‘𝐵)) |
81 | 9 | topontopi 20720 |
. . . . . . . 8
⊢ (𝐾 ×t 𝐾) ∈ Top |
82 | 81 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ×t 𝐾) ∈ Top) |
83 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) |
84 | 42, 83 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉):(𝐴 ∪ {𝐵})⟶(𝑋 × 𝑌)) |
85 | | toponuni 20719 |
. . . . . . . . . 10
⊢ ((𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) → (𝐴 ∪ {𝐵}) = ∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
86 | 65, 85 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ {𝐵}) = ∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
87 | 86 | feq2d 6031 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉):(𝐴 ∪ {𝐵})⟶(𝑋 × 𝑌) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶(𝑋 × 𝑌))) |
88 | 84, 87 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶(𝑋 × 𝑌)) |
89 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ (𝐾
↾t (𝐴
∪ {𝐵})) = ∪ (𝐾
↾t (𝐴
∪ {𝐵})) |
90 | 9 | toponunii 20721 |
. . . . . . . 8
⊢ (ℂ
× ℂ) = ∪ (𝐾 ×t 𝐾) |
91 | 89, 90 | cnprest2 21094 |
. . . . . . 7
⊢ (((𝐾 ×t 𝐾) ∈ Top ∧ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶(𝑋 × 𝑌) ∧ (𝑋 × 𝑌) ⊆ (ℂ × ℂ)) →
((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ×t 𝐾))‘𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)))‘𝐵))) |
92 | 82, 88, 13, 91 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ×t 𝐾))‘𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)))‘𝐵))) |
93 | 80, 92 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)))‘𝐵)) |
94 | 5 | oveq2i 6661 |
. . . . . 6
⊢ ((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽) = ((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌))) |
95 | 94 | fveq1i 6192 |
. . . . 5
⊢ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵) = (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)))‘𝐵) |
96 | 93, 95 | syl6eleqr 2712 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵)) |
97 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐶, 𝑅) = 𝐶) |
98 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐷, 𝑆) = 𝐷) |
99 | 97, 98 | opeq12d 4410 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉 = 〈𝐶, 𝐷〉) |
100 | | opex 4932 |
. . . . . . . 8
⊢
〈𝐶, 𝐷〉 ∈ V |
101 | 99, 83, 100 | fvmpt 6282 |
. . . . . . 7
⊢ (𝐵 ∈ (𝐴 ∪ {𝐵}) → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)‘𝐵) = 〈𝐶, 𝐷〉) |
102 | 69, 101 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)‘𝐵) = 〈𝐶, 𝐷〉) |
103 | 102 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)‘𝐵)) = ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) |
104 | 1, 103 | eleqtrrd 2704 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)‘𝐵))) |
105 | | cnpco 21071 |
. . . 4
⊢ (((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵) ∧ 𝐻 ∈ ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)‘𝐵))) → (𝐻 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
106 | 96, 104, 105 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐻 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ 〈if(𝑥 = 𝐵, 𝐶, 𝑅), if(𝑥 = 𝐵, 𝐷, 𝑆)〉)) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
107 | 53, 106 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
108 | 46 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
109 | 108, 33, 38 | fovrnd 6806 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅𝐻𝑆) ∈ ℂ) |
110 | 60, 61, 109, 72, 6 | limcmpt 23647 |
. 2
⊢ (𝜑 → ((𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐶𝐻𝐷), (𝑅𝐻𝑆))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
111 | 107, 110 | mpbird 247 |
1
⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵)) |