Proof of Theorem limcco
Step | Hyp | Ref
| Expression |
1 | | limcco.r |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 ≠ 𝐶)) → 𝑅 ∈ 𝐵) |
2 | 1 | expr 643 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 ≠ 𝐶 → 𝑅 ∈ 𝐵)) |
3 | 2 | necon1bd 2812 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑅 ∈ 𝐵 → 𝑅 = 𝐶)) |
4 | | limccl 23639 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋) ⊆ ℂ |
5 | | limcco.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋)) |
6 | 4, 5 | sseldi 3601 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
8 | | elsn2g 4210 |
. . . . . . . 8
⊢ (𝐶 ∈ ℂ → (𝑅 ∈ {𝐶} ↔ 𝑅 = 𝐶)) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 ∈ {𝐶} ↔ 𝑅 = 𝐶)) |
10 | 3, 9 | sylibrd 249 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑅 ∈ 𝐵 → 𝑅 ∈ {𝐶})) |
11 | 10 | orrd 393 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅 ∈ 𝐵 ∨ 𝑅 ∈ {𝐶})) |
12 | | elun 3753 |
. . . . 5
⊢ (𝑅 ∈ (𝐵 ∪ {𝐶}) ↔ (𝑅 ∈ 𝐵 ∨ 𝑅 ∈ {𝐶})) |
13 | 11, 12 | sylibr 224 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ (𝐵 ∪ {𝐶})) |
14 | | eqid 2622 |
. . . 4
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
15 | 13, 14 | fmptd 6385 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶(𝐵 ∪ {𝐶})) |
16 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ 𝑆) = (𝑦 ∈ 𝐵 ↦ 𝑆) |
17 | | limcco.s |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
18 | 16, 17 | dmmptd 6024 |
. . . . 5
⊢ (𝜑 → dom (𝑦 ∈ 𝐵 ↦ 𝑆) = 𝐵) |
19 | | limcco.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶)) |
20 | | limcrcl 23638 |
. . . . . . 7
⊢ (𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶) → ((𝑦 ∈ 𝐵 ↦ 𝑆):dom (𝑦 ∈ 𝐵 ↦ 𝑆)⟶ℂ ∧ dom (𝑦 ∈ 𝐵 ↦ 𝑆) ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
21 | 19, 20 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆):dom (𝑦 ∈ 𝐵 ↦ 𝑆)⟶ℂ ∧ dom (𝑦 ∈ 𝐵 ↦ 𝑆) ⊆ ℂ ∧ 𝐶 ∈ ℂ)) |
22 | 21 | simp2d 1074 |
. . . . 5
⊢ (𝜑 → dom (𝑦 ∈ 𝐵 ↦ 𝑆) ⊆ ℂ) |
23 | 18, 22 | eqsstr3d 3640 |
. . . 4
⊢ (𝜑 → 𝐵 ⊆ ℂ) |
24 | 6 | snssd 4340 |
. . . 4
⊢ (𝜑 → {𝐶} ⊆ ℂ) |
25 | 23, 24 | unssd 3789 |
. . 3
⊢ (𝜑 → (𝐵 ∪ {𝐶}) ⊆ ℂ) |
26 | | eqid 2622 |
. . 3
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
27 | | eqid 2622 |
. . 3
⊢
((TopOpen‘ℂfld) ↾t (𝐵 ∪ {𝐶})) = ((TopOpen‘ℂfld)
↾t (𝐵
∪ {𝐶})) |
28 | 23, 6, 17, 27, 26 | limcmpt 23647 |
. . . 4
⊢ (𝜑 → (𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶) ↔ (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∈
((((TopOpen‘ℂfld) ↾t (𝐵 ∪ {𝐶})) CnP
(TopOpen‘ℂfld))‘𝐶))) |
29 | 19, 28 | mpbid 222 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∈
((((TopOpen‘ℂfld) ↾t (𝐵 ∪ {𝐶})) CnP
(TopOpen‘ℂfld))‘𝐶)) |
30 | 15, 25, 26, 27, 5, 29 | limccnp 23655 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆))‘𝐶) ∈ (((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∘ (𝑥 ∈ 𝐴 ↦ 𝑅)) limℂ 𝑋)) |
31 | | ssun2 3777 |
. . . 4
⊢ {𝐶} ⊆ (𝐵 ∪ {𝐶}) |
32 | | snssg 4327 |
. . . . 5
⊢ (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝑋) → (𝐶 ∈ (𝐵 ∪ {𝐶}) ↔ {𝐶} ⊆ (𝐵 ∪ {𝐶}))) |
33 | 5, 32 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ (𝐵 ∪ {𝐶}) ↔ {𝐶} ⊆ (𝐵 ∪ {𝐶}))) |
34 | 31, 33 | mpbiri 248 |
. . 3
⊢ (𝜑 → 𝐶 ∈ (𝐵 ∪ {𝐶})) |
35 | | iftrue 4092 |
. . . 4
⊢ (𝑦 = 𝐶 → if(𝑦 = 𝐶, 𝐷, 𝑆) = 𝐷) |
36 | | eqid 2622 |
. . . 4
⊢ (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) = (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) |
37 | 35, 36 | fvmptg 6280 |
. . 3
⊢ ((𝐶 ∈ (𝐵 ∪ {𝐶}) ∧ 𝐷 ∈ ((𝑦 ∈ 𝐵 ↦ 𝑆) limℂ 𝐶)) → ((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆))‘𝐶) = 𝐷) |
38 | 34, 19, 37 | syl2anc 693 |
. 2
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆))‘𝐶) = 𝐷) |
39 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅)) |
40 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) = (𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆))) |
41 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑦 = 𝑅 → (𝑦 = 𝐶 ↔ 𝑅 = 𝐶)) |
42 | | limcco.1 |
. . . . . 6
⊢ (𝑦 = 𝑅 → 𝑆 = 𝑇) |
43 | 41, 42 | ifbieq2d 4111 |
. . . . 5
⊢ (𝑦 = 𝑅 → if(𝑦 = 𝐶, 𝐷, 𝑆) = if(𝑅 = 𝐶, 𝐷, 𝑇)) |
44 | 13, 39, 40, 43 | fmptco 6396 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∘ (𝑥 ∈ 𝐴 ↦ 𝑅)) = (𝑥 ∈ 𝐴 ↦ if(𝑅 = 𝐶, 𝐷, 𝑇))) |
45 | | ifid 4125 |
. . . . . 6
⊢ if(𝑅 = 𝐶, 𝑇, 𝑇) = 𝑇 |
46 | | limcco.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑅 = 𝐶)) → 𝑇 = 𝐷) |
47 | 46 | anassrs 680 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑅 = 𝐶) → 𝑇 = 𝐷) |
48 | 47 | ifeq1da 4116 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑅 = 𝐶, 𝑇, 𝑇) = if(𝑅 = 𝐶, 𝐷, 𝑇)) |
49 | 45, 48 | syl5reqr 2671 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → if(𝑅 = 𝐶, 𝐷, 𝑇) = 𝑇) |
50 | 49 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ if(𝑅 = 𝐶, 𝐷, 𝑇)) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
51 | 44, 50 | eqtrd 2656 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∘ (𝑥 ∈ 𝐴 ↦ 𝑅)) = (𝑥 ∈ 𝐴 ↦ 𝑇)) |
52 | 51 | oveq1d 6665 |
. 2
⊢ (𝜑 → (((𝑦 ∈ (𝐵 ∪ {𝐶}) ↦ if(𝑦 = 𝐶, 𝐷, 𝑆)) ∘ (𝑥 ∈ 𝐴 ↦ 𝑅)) limℂ 𝑋) = ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋)) |
53 | 30, 38, 52 | 3eltr3d 2715 |
1
⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑇) limℂ 𝑋)) |