Step | Hyp | Ref
| Expression |
1 | | limccnp.b |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶)) |
2 | | eqid 2622 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
3 | 2 | cnprcl 21049 |
. . . . . . . . 9
⊢ (𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶) → 𝐶 ∈ ∪ 𝐽) |
4 | 1, 3 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ∪ 𝐽) |
5 | | limccnp.j |
. . . . . . . . . 10
⊢ 𝐽 = (𝐾 ↾t 𝐷) |
6 | | limccnp.k |
. . . . . . . . . . . 12
⊢ 𝐾 =
(TopOpen‘ℂfld) |
7 | 6 | cnfldtopon 22586 |
. . . . . . . . . . 11
⊢ 𝐾 ∈
(TopOn‘ℂ) |
8 | | limccnp.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
9 | | resttopon 20965 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐷 ⊆ ℂ)
→ (𝐾
↾t 𝐷)
∈ (TopOn‘𝐷)) |
10 | 7, 8, 9 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 ↾t 𝐷) ∈ (TopOn‘𝐷)) |
11 | 5, 10 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐷)) |
12 | | toponuni 20719 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝐷) → 𝐷 = ∪ 𝐽) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 = ∪ 𝐽) |
14 | 4, 13 | eleqtrrd 2704 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝐷) |
15 | 14 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ 𝑥 = 𝐵) → 𝐶 ∈ 𝐷) |
16 | | limccnp.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶𝐷) |
17 | 16 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝐹:𝐴⟶𝐷) |
18 | | elun 3753 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵})) |
19 | | elsni 4194 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝐵} → 𝑥 = 𝐵) |
20 | 19 | orim2i 540 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐵}) → (𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵)) |
21 | 18, 20 | sylbi 207 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) → (𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵)) |
22 | 21 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (𝑥 ∈ 𝐴 ∨ 𝑥 = 𝐵)) |
23 | 22 | orcomd 403 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → (𝑥 = 𝐵 ∨ 𝑥 ∈ 𝐴)) |
24 | 23 | orcanai 952 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → 𝑥 ∈ 𝐴) |
25 | 17, 24 | ffvelrnd 6360 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → (𝐹‘𝑥) ∈ 𝐷) |
26 | 15, 25 | ifclda 4120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)) ∈ 𝐷) |
27 | | eqidd 2623 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) |
28 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℂ)) |
29 | | cnpf2 21054 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝐷) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘𝐶)) → 𝐺:𝐷⟶ℂ) |
30 | 11, 28, 1, 29 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → 𝐺:𝐷⟶ℂ) |
31 | 30 | feqmptd 6249 |
. . . . 5
⊢ (𝜑 → 𝐺 = (𝑦 ∈ 𝐷 ↦ (𝐺‘𝑦))) |
32 | | fveq2 6191 |
. . . . 5
⊢ (𝑦 = if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)) → (𝐺‘𝑦) = (𝐺‘if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) |
33 | 26, 27, 31, 32 | fmptco 6396 |
. . . 4
⊢ (𝜑 → (𝐺 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ (𝐺‘if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))))) |
34 | | fvco3 6275 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐷 ∧ 𝑥 ∈ 𝐴) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
35 | 17, 24, 34 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) ∧ ¬ 𝑥 = 𝐵) → ((𝐺 ∘ 𝐹)‘𝑥) = (𝐺‘(𝐹‘𝑥))) |
36 | 35 | ifeq2da 4117 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥)) = if(𝑥 = 𝐵, (𝐺‘𝐶), (𝐺‘(𝐹‘𝑥)))) |
37 | | fvif 6204 |
. . . . . 6
⊢ (𝐺‘if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) = if(𝑥 = 𝐵, (𝐺‘𝐶), (𝐺‘(𝐹‘𝑥))) |
38 | 36, 37 | syl6eqr 2674 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ {𝐵})) → if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥)) = (𝐺‘if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) |
39 | 38 | mpteq2dva 4744 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ (𝐺‘if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))))) |
40 | 33, 39 | eqtr4d 2659 |
. . 3
⊢ (𝜑 → (𝐺 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥)))) |
41 | | limccnp.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ (𝐹 limℂ 𝐵)) |
42 | | eqid 2622 |
. . . . . . . 8
⊢ (𝐾 ↾t (𝐴 ∪ {𝐵})) = (𝐾 ↾t (𝐴 ∪ {𝐵})) |
43 | | eqid 2622 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) |
44 | 16, 8 | fssd 6057 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
45 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐷 → dom 𝐹 = 𝐴) |
46 | 16, 45 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
47 | | limcrcl 23638 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
48 | 41, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
49 | 48 | simp2d 1074 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 ⊆ ℂ) |
50 | 46, 49 | eqsstr3d 3640 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
51 | 48 | simp3d 1075 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℂ) |
52 | 42, 6, 43, 44, 50, 51 | ellimc 23637 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ (𝐹 limℂ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
53 | 41, 52 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
54 | 6 | cnfldtop 22587 |
. . . . . . . 8
⊢ 𝐾 ∈ Top |
55 | 54 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
56 | 26, 43 | fmptd 6385 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))):(𝐴 ∪ {𝐵})⟶𝐷) |
57 | 51 | snssd 4340 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝐵} ⊆ ℂ) |
58 | 50, 57 | unssd 3789 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∪ {𝐵}) ⊆ ℂ) |
59 | | resttopon 20965 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ (𝐴 ∪ {𝐵}) ⊆ ℂ) →
(𝐾 ↾t
(𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
60 | 7, 58, 59 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵}))) |
61 | | toponuni 20719 |
. . . . . . . . . 10
⊢ ((𝐾 ↾t (𝐴 ∪ {𝐵})) ∈ (TopOn‘(𝐴 ∪ {𝐵})) → (𝐴 ∪ {𝐵}) = ∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∪ {𝐵}) = ∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))) |
63 | 62 | feq2d 6031 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))):(𝐴 ∪ {𝐵})⟶𝐷 ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶𝐷)) |
64 | 56, 63 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶𝐷) |
65 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ (𝐾
↾t (𝐴
∪ {𝐵})) = ∪ (𝐾
↾t (𝐴
∪ {𝐵})) |
66 | 7 | toponunii 20721 |
. . . . . . . 8
⊢ ℂ =
∪ 𝐾 |
67 | 65, 66 | cnprest2 21094 |
. . . . . . 7
⊢ ((𝐾 ∈ Top ∧ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))):∪ (𝐾 ↾t (𝐴 ∪ {𝐵}))⟶𝐷 ∧ 𝐷 ⊆ ℂ) → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ↾t 𝐷))‘𝐵))) |
68 | 55, 64, 8, 67 | syl3anc 1326 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ↾t 𝐷))‘𝐵))) |
69 | 53, 68 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ↾t 𝐷))‘𝐵)) |
70 | 5 | oveq2i 6661 |
. . . . . 6
⊢ ((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽) = ((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ↾t 𝐷)) |
71 | 70 | fveq1i 6192 |
. . . . 5
⊢ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵) = (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP (𝐾 ↾t 𝐷))‘𝐵) |
72 | 69, 71 | syl6eleqr 2712 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵)) |
73 | | ssun2 3777 |
. . . . . . . 8
⊢ {𝐵} ⊆ (𝐴 ∪ {𝐵}) |
74 | | snssg 4327 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℂ → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
75 | 51, 74 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 ∈ (𝐴 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝐴 ∪ {𝐵}))) |
76 | 73, 75 | mpbiri 248 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (𝐴 ∪ {𝐵})) |
77 | | iftrue 4092 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)) = 𝐶) |
78 | 77, 43 | fvmptg 6280 |
. . . . . . 7
⊢ ((𝐵 ∈ (𝐴 ∪ {𝐵}) ∧ 𝐶 ∈ 𝐷) → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))‘𝐵) = 𝐶) |
79 | 76, 14, 78 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))‘𝐵) = 𝐶) |
80 | 79 | fveq2d 6195 |
. . . . 5
⊢ (𝜑 → ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))‘𝐵)) = ((𝐽 CnP 𝐾)‘𝐶)) |
81 | 1, 80 | eleqtrrd 2704 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))‘𝐵))) |
82 | | cnpco 21071 |
. . . 4
⊢ (((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐽)‘𝐵) ∧ 𝐺 ∈ ((𝐽 CnP 𝐾)‘((𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))‘𝐵))) → (𝐺 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
83 | 72, 81, 82 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐺 ∘ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, 𝐶, (𝐹‘𝑥)))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
84 | 40, 83 | eqeltrrd 2702 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵)) |
85 | | eqid 2622 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥))) = (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥))) |
86 | | fco 6058 |
. . . 4
⊢ ((𝐺:𝐷⟶ℂ ∧ 𝐹:𝐴⟶𝐷) → (𝐺 ∘ 𝐹):𝐴⟶ℂ) |
87 | 30, 16, 86 | syl2anc 693 |
. . 3
⊢ (𝜑 → (𝐺 ∘ 𝐹):𝐴⟶ℂ) |
88 | 42, 6, 85, 87, 50, 51 | ellimc 23637 |
. 2
⊢ (𝜑 → ((𝐺‘𝐶) ∈ ((𝐺 ∘ 𝐹) limℂ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ {𝐵}) ↦ if(𝑥 = 𝐵, (𝐺‘𝐶), ((𝐺 ∘ 𝐹)‘𝑥))) ∈ (((𝐾 ↾t (𝐴 ∪ {𝐵})) CnP 𝐾)‘𝐵))) |
89 | 84, 88 | mpbird 247 |
1
⊢ (𝜑 → (𝐺‘𝐶) ∈ ((𝐺 ∘ 𝐹) limℂ 𝐵)) |