Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  limciun Structured version   Visualization version   GIF version

Theorem limciun 24497
 Description: A point is a limit of 𝐹 on the finite union ∪ 𝑥 ∈ 𝐴𝐵(𝑥) iff it is the limit of the restriction of 𝐹 to each 𝐵(𝑥). (Contributed by Mario Carneiro, 30-Dec-2016.)
Hypotheses
Ref Expression
limciun.1 (𝜑𝐴 ∈ Fin)
limciun.2 (𝜑 → ∀𝑥𝐴 𝐵 ⊆ ℂ)
limciun.3 (𝜑𝐹: 𝑥𝐴 𝐵⟶ℂ)
limciun.4 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
limciun (𝜑 → (𝐹 lim 𝐶) = (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐹
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem limciun
Dummy variables 𝑔 𝑎 𝑘 𝑢 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 limccl 24478 . . . 4 (𝐹 lim 𝐶) ⊆ ℂ
2 limcresi 24488 . . . . . 6 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶)
32rgenw 3118 . . . . 5 𝑥𝐴 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶)
4 ssiin 4942 . . . . 5 ((𝐹 lim 𝐶) ⊆ 𝑥𝐴 ((𝐹𝐵) lim 𝐶) ↔ ∀𝑥𝐴 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶))
53, 4mpbir 234 . . . 4 (𝐹 lim 𝐶) ⊆ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)
61, 5ssini 4158 . . 3 (𝐹 lim 𝐶) ⊆ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶))
76a1i 11 . 2 (𝜑 → (𝐹 lim 𝐶) ⊆ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)))
8 elriin 4966 . . . 4 (𝑦 ∈ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) ↔ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶)))
9 simprl 770 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑦 ∈ ℂ)
10 limciun.1 . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
1110ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → 𝐴 ∈ Fin)
12 simplrr 777 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))
13 nfcv 2955 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐹
14 nfcsb1v 3852 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑎 / 𝑥𝐵
1513, 14nfres 5820 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑎 / 𝑥𝐵)
16 nfcv 2955 . . . . . . . . . . . . . . . . . . 19 𝑥 lim
17 nfcv 2955 . . . . . . . . . . . . . . . . . . 19 𝑥𝐶
1815, 16, 17nfov 7165 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑎 / 𝑥𝐵) lim 𝐶)
1918nfcri 2943 . . . . . . . . . . . . . . . . 17 𝑥 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)
20 csbeq1a 3842 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎𝐵 = 𝑎 / 𝑥𝐵)
2120reseq2d 5818 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝐹𝐵) = (𝐹𝑎 / 𝑥𝐵))
2221oveq1d 7150 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ((𝐹𝐵) lim 𝐶) = ((𝐹𝑎 / 𝑥𝐵) lim 𝐶))
2322eleq2d 2875 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝑦 ∈ ((𝐹𝐵) lim 𝐶) ↔ 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)))
2419, 23rspc 3559 . . . . . . . . . . . . . . . 16 (𝑎𝐴 → (∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶) → 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)))
2512, 24mpan9 510 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶))
26 limciun.3 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹: 𝑥𝐴 𝐵⟶ℂ)
2726ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝐹: 𝑥𝐴 𝐵⟶ℂ)
28 ssiun2 4934 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴𝑎 / 𝑥𝐵 𝑎𝐴 𝑎 / 𝑥𝐵)
29 nfcv 2955 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
3029, 14, 20cbviun 4923 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐴 𝐵 = 𝑎𝐴 𝑎 / 𝑥𝐵
3128, 30sseqtrrdi 3966 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴𝑎 / 𝑥𝐵 𝑥𝐴 𝐵)
3231adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎 / 𝑥𝐵 𝑥𝐴 𝐵)
3327, 32fssresd 6519 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → (𝐹𝑎 / 𝑥𝐵):𝑎 / 𝑥𝐵⟶ℂ)
34 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎𝐴)
35 limciun.2 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴 𝐵 ⊆ ℂ)
3635ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → ∀𝑥𝐴 𝐵 ⊆ ℂ)
37 nfcv 2955 . . . . . . . . . . . . . . . . . . . 20 𝑥
3814, 37nfss 3907 . . . . . . . . . . . . . . . . . . 19 𝑥𝑎 / 𝑥𝐵 ⊆ ℂ
3920sseq1d 3946 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝐵 ⊆ ℂ ↔ 𝑎 / 𝑥𝐵 ⊆ ℂ))
4038, 39rspc 3559 . . . . . . . . . . . . . . . . . 18 (𝑎𝐴 → (∀𝑥𝐴 𝐵 ⊆ ℂ → 𝑎 / 𝑥𝐵 ⊆ ℂ))
4134, 36, 40sylc 65 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎 / 𝑥𝐵 ⊆ ℂ)
42 limciun.4 . . . . . . . . . . . . . . . . . 18 (𝜑𝐶 ∈ ℂ)
4342ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝐶 ∈ ℂ)
44 eqid 2798 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4533, 41, 43, 44ellimc2 24480 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → (𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
4645adantlr 714 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → (𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
4725, 46mpbid 235 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))))
4847simprd 499 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
49 simplrl 776 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑢 ∈ (TopOpen‘ℂfld))
50 simplrr 777 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑦𝑢)
51 rsp 3170 . . . . . . . . . . . . 13 (∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → (𝑢 ∈ (TopOpen‘ℂfld) → (𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))))
5248, 49, 50, 51syl3c 66 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
5352ralrimiva 3149 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑎𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
54 nfv 1915 . . . . . . . . . . . 12 𝑎𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)
55 nfcv 2955 . . . . . . . . . . . . 13 𝑥(TopOpen‘ℂfld)
56 nfv 1915 . . . . . . . . . . . . . 14 𝑥 𝐶𝑘
57 nfcv 2955 . . . . . . . . . . . . . . . . 17 𝑥𝑘
58 nfcv 2955 . . . . . . . . . . . . . . . . . 18 𝑥{𝐶}
5914, 58nfdif 4053 . . . . . . . . . . . . . . . . 17 𝑥(𝑎 / 𝑥𝐵 ∖ {𝐶})
6057, 59nfin 4143 . . . . . . . . . . . . . . . 16 𝑥(𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))
6115, 60nfima 5904 . . . . . . . . . . . . . . 15 𝑥((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶})))
62 nfcv 2955 . . . . . . . . . . . . . . 15 𝑥𝑢
6361, 62nfss 3907 . . . . . . . . . . . . . 14 𝑥((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢
6456, 63nfan 1900 . . . . . . . . . . . . 13 𝑥(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)
6555, 64nfrex 3268 . . . . . . . . . . . 12 𝑥𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)
6620difeq1d 4049 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐵 ∖ {𝐶}) = (𝑎 / 𝑥𝐵 ∖ {𝐶}))
6766ineq2d 4139 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (𝑘 ∩ (𝐵 ∖ {𝐶})) = (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶})))
6821, 67imaeq12d 5897 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))))
6968sseq1d 3946 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7069anbi2d 631 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7170rexbidv 3256 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7254, 65, 71cbvralw 3387 . . . . . . . . . . 11 (∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∀𝑎𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7353, 72sylibr 237 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))
74 eleq2 2878 . . . . . . . . . . . 12 (𝑘 = (𝑔𝑥) → (𝐶𝑘𝐶 ∈ (𝑔𝑥)))
75 ineq1 4131 . . . . . . . . . . . . . 14 (𝑘 = (𝑔𝑥) → (𝑘 ∩ (𝐵 ∖ {𝐶})) = ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶})))
7675imaeq2d 5896 . . . . . . . . . . . . 13 (𝑘 = (𝑔𝑥) → ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))))
7776sseq1d 3946 . . . . . . . . . . . 12 (𝑘 = (𝑔𝑥) → (((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7874, 77anbi12d 633 . . . . . . . . . . 11 (𝑘 = (𝑔𝑥) → ((𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7978ac6sfi 8746 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
8011, 73, 79syl2anc 587 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
8144cnfldtop 23389 . . . . . . . . . . 11 (TopOpen‘ℂfld) ∈ Top
82 frn 6493 . . . . . . . . . . . 12 (𝑔:𝐴⟶(TopOpen‘ℂfld) → ran 𝑔 ⊆ (TopOpen‘ℂfld))
8382ad2antrl 727 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ⊆ (TopOpen‘ℂfld))
8411adantr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐴 ∈ Fin)
85 ffn 6487 . . . . . . . . . . . . . 14 (𝑔:𝐴⟶(TopOpen‘ℂfld) → 𝑔 Fn 𝐴)
8685ad2antrl 727 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔 Fn 𝐴)
87 dffn4 6571 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴𝑔:𝐴onto→ran 𝑔)
8886, 87sylib 221 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔:𝐴onto→ran 𝑔)
89 fofi 8794 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ 𝑔:𝐴onto→ran 𝑔) → ran 𝑔 ∈ Fin)
9084, 88, 89syl2anc 587 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ∈ Fin)
91 unicntop 23391 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
9291rintopn 21514 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ ran 𝑔 ⊆ (TopOpen‘ℂfld) ∧ ran 𝑔 ∈ Fin) → (ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld))
9381, 83, 90, 92mp3an2i 1463 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld))
9442adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝐶 ∈ ℂ)
9594ad2antrr 725 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ ℂ)
96 simpl 486 . . . . . . . . . . . . . 14 ((𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → 𝐶 ∈ (𝑔𝑥))
9796ralimi 3128 . . . . . . . . . . . . 13 (∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥))
9897ad2antll 728 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥))
99 eleq2 2878 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝑥) → (𝐶𝑧𝐶 ∈ (𝑔𝑥)))
10099ralrn 6831 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝐶𝑧 ↔ ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥)))
10186, 100syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (∀𝑧 ∈ ran 𝑔 𝐶𝑧 ↔ ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥)))
10298, 101mpbird 260 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑧 ∈ ran 𝑔 𝐶𝑧)
103 elrint 4879 . . . . . . . . . . 11 (𝐶 ∈ (ℂ ∩ ran 𝑔) ↔ (𝐶 ∈ ℂ ∧ ∀𝑧 ∈ ran 𝑔 𝐶𝑧))
10495, 102, 103sylanbrc 586 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ (ℂ ∩ ran 𝑔))
105 indifcom 4199 . . . . . . . . . . . . . 14 ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = ( 𝑥𝐴 𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
106 iunin1 4957 . . . . . . . . . . . . . 14 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) = ( 𝑥𝐴 𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
107105, 106eqtr4i 2824 . . . . . . . . . . . . 13 ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
108107imaeq2i 5894 . . . . . . . . . . . 12 (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = (𝐹 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
109 imaiun 6982 . . . . . . . . . . . 12 (𝐹 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) = 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
110108, 109eqtri 2821 . . . . . . . . . . 11 (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
111 inss2 4156 . . . . . . . . . . . . . . . . . . . . 21 (ℂ ∩ ran 𝑔) ⊆ ran 𝑔
112 fnfvelrn 6825 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 Fn 𝐴𝑥𝐴) → (𝑔𝑥) ∈ ran 𝑔)
11385, 112sylan 583 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ran 𝑔)
114 intss1 4853 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔𝑥) ∈ ran 𝑔 ran 𝑔 ⊆ (𝑔𝑥))
115113, 114syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ran 𝑔 ⊆ (𝑔𝑥))
116111, 115sstrid 3926 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (ℂ ∩ ran 𝑔) ⊆ (𝑔𝑥))
117116ssdifd 4068 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ((ℂ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔𝑥) ∖ {𝐶}))
118 sslin 4161 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔𝑥) ∖ {𝐶}) → (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
119 imass2 5932 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
120117, 118, 1193syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
121 indifcom 4199 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶})) = (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))
122121imaeq2i 5894 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
123 inss1 4155 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) ⊆ 𝐵
124 resima2 5853 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) ⊆ 𝐵 → ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
125123, 124ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
126122, 125eqtri 2821 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
127120, 126sseqtrrdi 3966 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))))
128 sstr2 3922 . . . . . . . . . . . . . . . . 17 ((𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) → (((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
129127, 128syl 17 . . . . . . . . . . . . . . . 16 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
130129adantld 494 . . . . . . . . . . . . . . 15 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ((𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
131130ralimdva 3144 . . . . . . . . . . . . . 14 (𝑔:𝐴⟶(TopOpen‘ℂfld) → (∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
132131imp 410 . . . . . . . . . . . . 13 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
133132adantl 485 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
134 iunss 4932 . . . . . . . . . . . 12 ( 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢 ↔ ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
135133, 134sylibr 237 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
136110, 135eqsstrid 3963 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)
137 eleq2 2878 . . . . . . . . . . . 12 (𝑣 = (ℂ ∩ ran 𝑔) → (𝐶𝑣𝐶 ∈ (ℂ ∩ ran 𝑔)))
138 ineq1 4131 . . . . . . . . . . . . . 14 (𝑣 = (ℂ ∩ ran 𝑔) → (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})))
139138imaeq2d 5896 . . . . . . . . . . . . 13 (𝑣 = (ℂ ∩ ran 𝑔) → (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))))
140139sseq1d 3946 . . . . . . . . . . . 12 (𝑣 = (ℂ ∩ ran 𝑔) → ((𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
141137, 140anbi12d 633 . . . . . . . . . . 11 (𝑣 = (ℂ ∩ ran 𝑔) → ((𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (ℂ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
142141rspcev 3571 . . . . . . . . . 10 (((ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld) ∧ (𝐶 ∈ (ℂ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
14393, 104, 136, 142syl12anc 835 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
14480, 143exlimddv 1936 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
145144expr 460 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑢 ∈ (TopOpen‘ℂfld)) → (𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
146145ralrimiva 3149 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
14726adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝐹: 𝑥𝐴 𝐵⟶ℂ)
148 iunss 4932 . . . . . . . . 9 ( 𝑥𝐴 𝐵 ⊆ ℂ ↔ ∀𝑥𝐴 𝐵 ⊆ ℂ)
14935, 148sylibr 237 . . . . . . . 8 (𝜑 𝑥𝐴 𝐵 ⊆ ℂ)
150149adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑥𝐴 𝐵 ⊆ ℂ)
151147, 150, 94, 44ellimc2 24480 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → (𝑦 ∈ (𝐹 lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
1529, 146, 151mpbir2and 712 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑦 ∈ (𝐹 lim 𝐶))
153152ex 416 . . . 4 (𝜑 → ((𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶)) → 𝑦 ∈ (𝐹 lim 𝐶)))
1548, 153syl5bi 245 . . 3 (𝜑 → (𝑦 ∈ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) → 𝑦 ∈ (𝐹 lim 𝐶)))
155154ssrdv 3921 . 2 (𝜑 → (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) ⊆ (𝐹 lim 𝐶))
1567, 155eqssd 3932 1 (𝜑 → (𝐹 lim 𝐶) = (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  ⦋csb 3828   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  {csn 4525  ∩ cint 4838  ∪ ciun 4881  ∩ ciin 4882  ran crn 5520   ↾ cres 5521   “ cima 5522   Fn wfn 6319  ⟶wf 6320  –onto→wfo 6322  ‘cfv 6324  (class class class)co 7135  Fincfn 8492  ℂcc 10524  TopOpenctopn 16687  ℂfldccnfld 20091  Topctop 21498   limℂ climc 24465 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fi 8859  df-sup 8890  df-inf 8891  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-fz 12886  df-seq 13365  df-exp 13426  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-plusg 16570  df-mulr 16571  df-starv 16572  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-rest 16688  df-topn 16689  df-topgen 16709  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cnp 21833  df-xms 22927  df-ms 22928  df-limc 24469 This theorem is referenced by:  limcun  24498
 Copyright terms: Public domain W3C validator