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

Theorem limciun 23464
 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 23445 . . . 4 (𝐹 lim 𝐶) ⊆ ℂ
2 limcresi 23455 . . . . . 6 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶)
32rgenw 2908 . . . . 5 𝑥𝐴 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶)
4 ssiin 4506 . . . . 5 ((𝐹 lim 𝐶) ⊆ 𝑥𝐴 ((𝐹𝐵) lim 𝐶) ↔ ∀𝑥𝐴 (𝐹 lim 𝐶) ⊆ ((𝐹𝐵) lim 𝐶))
53, 4mpbir 220 . . . 4 (𝐹 lim 𝐶) ⊆ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)
61, 5ssini 3798 . . 3 (𝐹 lim 𝐶) ⊆ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶))
76a1i 11 . 2 (𝜑 → (𝐹 lim 𝐶) ⊆ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)))
8 elriin 4529 . . . 4 (𝑦 ∈ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) ↔ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶)))
9 simprl 790 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑦 ∈ ℂ)
10 limciun.1 . . . . . . . . . . 11 (𝜑𝐴 ∈ Fin)
1110ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → 𝐴 ∈ Fin)
12 simplrr 797 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))
13 nfcv 2751 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐹
14 nfcsb1v 3515 . . . . . . . . . . . . . . . . . . . 20 𝑥𝑎 / 𝑥𝐵
1513, 14nfres 5319 . . . . . . . . . . . . . . . . . . 19 𝑥(𝐹𝑎 / 𝑥𝐵)
16 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑥 lim
17 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 𝑥𝐶
1815, 16, 17nfov 6575 . . . . . . . . . . . . . . . . . 18 𝑥((𝐹𝑎 / 𝑥𝐵) lim 𝐶)
1918nfcri 2745 . . . . . . . . . . . . . . . . 17 𝑥 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)
20 csbeq1a 3508 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑎𝐵 = 𝑎 / 𝑥𝐵)
2120reseq2d 5317 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝐹𝐵) = (𝐹𝑎 / 𝑥𝐵))
2221oveq1d 6564 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ((𝐹𝐵) lim 𝐶) = ((𝐹𝑎 / 𝑥𝐵) lim 𝐶))
2322eleq2d 2673 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝑦 ∈ ((𝐹𝐵) lim 𝐶) ↔ 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)))
2419, 23rspc 3276 . . . . . . . . . . . . . . . 16 (𝑎𝐴 → (∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶) → 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶)))
2512, 24mpan9 485 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶))
26 limciun.3 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐹: 𝑥𝐴 𝐵⟶ℂ)
2726ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝐹: 𝑥𝐴 𝐵⟶ℂ)
28 ssiun2 4499 . . . . . . . . . . . . . . . . . . . 20 (𝑎𝐴𝑎 / 𝑥𝐵 𝑎𝐴 𝑎 / 𝑥𝐵)
29 nfcv 2751 . . . . . . . . . . . . . . . . . . . . 21 𝑎𝐵
3029, 14, 20cbviun 4493 . . . . . . . . . . . . . . . . . . . 20 𝑥𝐴 𝐵 = 𝑎𝐴 𝑎 / 𝑥𝐵
3128, 30syl6sseqr 3615 . . . . . . . . . . . . . . . . . . 19 (𝑎𝐴𝑎 / 𝑥𝐵 𝑥𝐴 𝐵)
3231adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎 / 𝑥𝐵 𝑥𝐴 𝐵)
3327, 32fssresd 5984 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → (𝐹𝑎 / 𝑥𝐵):𝑎 / 𝑥𝐵⟶ℂ)
34 simpr 476 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎𝐴)
35 limciun.2 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ∀𝑥𝐴 𝐵 ⊆ ℂ)
3635ad2antrr 758 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → ∀𝑥𝐴 𝐵 ⊆ ℂ)
37 nfcv 2751 . . . . . . . . . . . . . . . . . . . 20 𝑥
3814, 37nfss 3561 . . . . . . . . . . . . . . . . . . 19 𝑥𝑎 / 𝑥𝐵 ⊆ ℂ
3920sseq1d 3595 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝐵 ⊆ ℂ ↔ 𝑎 / 𝑥𝐵 ⊆ ℂ))
4038, 39rspc 3276 . . . . . . . . . . . . . . . . . 18 (𝑎𝐴 → (∀𝑥𝐴 𝐵 ⊆ ℂ → 𝑎 / 𝑥𝐵 ⊆ ℂ))
4134, 36, 40sylc 63 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝑎 / 𝑥𝐵 ⊆ ℂ)
42 limciun.4 . . . . . . . . . . . . . . . . . 18 (𝜑𝐶 ∈ ℂ)
4342ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → 𝐶 ∈ ℂ)
44 eqid 2610 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4533, 41, 43, 44ellimc2 23447 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑎𝐴) → (𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
4645adantlr 747 . . . . . . . . . . . . . . 15 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → (𝑦 ∈ ((𝐹𝑎 / 𝑥𝐵) lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
4725, 46mpbid 221 . . . . . . . . . . . . . 14 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))))
4847simprd 478 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
49 simplrl 796 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑢 ∈ (TopOpen‘ℂfld))
50 simplrr 797 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → 𝑦𝑢)
51 rsp 2913 . . . . . . . . . . . . 13 (∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → (𝑢 ∈ (TopOpen‘ℂfld) → (𝑦𝑢 → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))))
5248, 49, 50, 51syl3c 64 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ 𝑎𝐴) → ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
5352ralrimiva 2949 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑎𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
54 nfv 1830 . . . . . . . . . . . 12 𝑎𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)
55 nfcv 2751 . . . . . . . . . . . . 13 𝑥(TopOpen‘ℂfld)
56 nfv 1830 . . . . . . . . . . . . . 14 𝑥 𝐶𝑘
57 nfcv 2751 . . . . . . . . . . . . . . . . 17 𝑥𝑘
58 nfcv 2751 . . . . . . . . . . . . . . . . . 18 𝑥{𝐶}
5914, 58nfdif 3693 . . . . . . . . . . . . . . . . 17 𝑥(𝑎 / 𝑥𝐵 ∖ {𝐶})
6057, 59nfin 3782 . . . . . . . . . . . . . . . 16 𝑥(𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))
6115, 60nfima 5393 . . . . . . . . . . . . . . 15 𝑥((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶})))
62 nfcv 2751 . . . . . . . . . . . . . . 15 𝑥𝑢
6361, 62nfss 3561 . . . . . . . . . . . . . 14 𝑥((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢
6456, 63nfan 1816 . . . . . . . . . . . . 13 𝑥(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)
6555, 64nfrex 2990 . . . . . . . . . . . 12 𝑥𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)
6620difeq1d 3689 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝐵 ∖ {𝐶}) = (𝑎 / 𝑥𝐵 ∖ {𝐶}))
6766ineq2d 3776 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (𝑘 ∩ (𝐵 ∖ {𝐶})) = (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶})))
6821, 67imaeq12d 5386 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))))
6968sseq1d 3595 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7069anbi2d 736 . . . . . . . . . . . . 13 (𝑥 = 𝑎 → ((𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7170rexbidv 3034 . . . . . . . . . . . 12 (𝑥 = 𝑎 → (∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∃𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7254, 65, 71cbvral 3143 . . . . . . . . . . 11 (∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ ∀𝑎𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝑎 / 𝑥𝐵) “ (𝑘 ∩ (𝑎 / 𝑥𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7353, 72sylibr 223 . . . . . . . . . 10 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))
74 eleq2 2677 . . . . . . . . . . . 12 (𝑘 = (𝑔𝑥) → (𝐶𝑘𝐶 ∈ (𝑔𝑥)))
75 ineq1 3769 . . . . . . . . . . . . . 14 (𝑘 = (𝑔𝑥) → (𝑘 ∩ (𝐵 ∖ {𝐶})) = ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶})))
7675imaeq2d 5385 . . . . . . . . . . . . 13 (𝑘 = (𝑔𝑥) → ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))))
7776sseq1d 3595 . . . . . . . . . . . 12 (𝑘 = (𝑔𝑥) → (((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))
7874, 77anbi12d 743 . . . . . . . . . . 11 (𝑘 = (𝑔𝑥) → ((𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
7978ac6sfi 8089 . . . . . . . . . 10 ((𝐴 ∈ Fin ∧ ∀𝑥𝐴𝑘 ∈ (TopOpen‘ℂfld)(𝐶𝑘 ∧ ((𝐹𝐵) “ (𝑘 ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
8011, 73, 79syl2anc 691 . . . . . . . . 9 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∃𝑔(𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
8144cnfldtop 22397 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ Top
8281a1i 11 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (TopOpen‘ℂfld) ∈ Top)
83 frn 5966 . . . . . . . . . . . 12 (𝑔:𝐴⟶(TopOpen‘ℂfld) → ran 𝑔 ⊆ (TopOpen‘ℂfld))
8483ad2antrl 760 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ⊆ (TopOpen‘ℂfld))
8511adantr 480 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐴 ∈ Fin)
86 ffn 5958 . . . . . . . . . . . . . 14 (𝑔:𝐴⟶(TopOpen‘ℂfld) → 𝑔 Fn 𝐴)
8786ad2antrl 760 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔 Fn 𝐴)
88 dffn4 6034 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴𝑔:𝐴onto→ran 𝑔)
8987, 88sylib 207 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑔:𝐴onto→ran 𝑔)
90 fofi 8135 . . . . . . . . . . . 12 ((𝐴 ∈ Fin ∧ 𝑔:𝐴onto→ran 𝑔) → ran 𝑔 ∈ Fin)
9185, 89, 90syl2anc 691 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ran 𝑔 ∈ Fin)
9244cnfldtopon 22396 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
9392toponunii 20547 . . . . . . . . . . . 12 ℂ = (TopOpen‘ℂfld)
9493rintopn 20539 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ ran 𝑔 ⊆ (TopOpen‘ℂfld) ∧ ran 𝑔 ∈ Fin) → (ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld))
9582, 84, 91, 94syl3anc 1318 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld))
9642adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝐶 ∈ ℂ)
9796ad2antrr 758 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ ℂ)
98 simpl 472 . . . . . . . . . . . . . 14 ((𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → 𝐶 ∈ (𝑔𝑥))
9998ralimi 2936 . . . . . . . . . . . . 13 (∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥))
10099ad2antll 761 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥))
101 eleq2 2677 . . . . . . . . . . . . . 14 (𝑧 = (𝑔𝑥) → (𝐶𝑧𝐶 ∈ (𝑔𝑥)))
102101ralrn 6270 . . . . . . . . . . . . 13 (𝑔 Fn 𝐴 → (∀𝑧 ∈ ran 𝑔 𝐶𝑧 ↔ ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥)))
10387, 102syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (∀𝑧 ∈ ran 𝑔 𝐶𝑧 ↔ ∀𝑥𝐴 𝐶 ∈ (𝑔𝑥)))
104100, 103mpbird 246 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑧 ∈ ran 𝑔 𝐶𝑧)
105 elrint 4453 . . . . . . . . . . 11 (𝐶 ∈ (ℂ ∩ ran 𝑔) ↔ (𝐶 ∈ ℂ ∧ ∀𝑧 ∈ ran 𝑔 𝐶𝑧))
10697, 104, 105sylanbrc 695 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝐶 ∈ (ℂ ∩ ran 𝑔))
107 indifcom 3831 . . . . . . . . . . . . . 14 ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = ( 𝑥𝐴 𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
108 iunin1 4521 . . . . . . . . . . . . . 14 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) = ( 𝑥𝐴 𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
109107, 108eqtr4i 2635 . . . . . . . . . . . . 13 ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))
110109imaeq2i 5383 . . . . . . . . . . . 12 (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = (𝐹 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
111 imaiun 6407 . . . . . . . . . . . 12 (𝐹 𝑥𝐴 (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) = 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
112110, 111eqtri 2632 . . . . . . . . . . 11 (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})))
113 inss2 3796 . . . . . . . . . . . . . . . . . . . . 21 (ℂ ∩ ran 𝑔) ⊆ ran 𝑔
114 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔 Fn 𝐴𝑥𝐴) → (𝑔𝑥) ∈ ran 𝑔)
11586, 114sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝑔𝑥) ∈ ran 𝑔)
116 intss1 4427 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔𝑥) ∈ ran 𝑔 ran 𝑔 ⊆ (𝑔𝑥))
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ran 𝑔 ⊆ (𝑔𝑥))
118113, 117syl5ss 3579 . . . . . . . . . . . . . . . . . . . 20 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (ℂ ∩ ran 𝑔) ⊆ (𝑔𝑥))
119118ssdifd 3708 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ((ℂ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔𝑥) ∖ {𝐶}))
120 sslin 3801 . . . . . . . . . . . . . . . . . . 19 (((ℂ ∩ ran 𝑔) ∖ {𝐶}) ⊆ ((𝑔𝑥) ∖ {𝐶}) → (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
121 imass2 5420 . . . . . . . . . . . . . . . . . . 19 ((𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶})) ⊆ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
122119, 120, 1213syl 18 . . . . . . . . . . . . . . . . . 18 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
123 indifcom 3831 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶})) = (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))
124123imaeq2i 5383 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) = ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
125 inss1 3795 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) ⊆ 𝐵
126 resima2 5352 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})) ⊆ 𝐵 → ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))))
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝐵) “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
128124, 127eqtri 2632 . . . . . . . . . . . . . . . . . 18 ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) = (𝐹 “ (𝐵 ∩ ((𝑔𝑥) ∖ {𝐶})))
129122, 128syl6sseqr 3615 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))))
130 sstr2 3575 . . . . . . . . . . . . . . . . 17 ((𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) → (((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
131129, 130syl 17 . . . . . . . . . . . . . . . 16 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → (((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢 → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
132131adantld 482 . . . . . . . . . . . . . . 15 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ 𝑥𝐴) → ((𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
133132ralimdva 2945 . . . . . . . . . . . . . 14 (𝑔:𝐴⟶(TopOpen‘ℂfld) → (∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢))
134133imp 444 . . . . . . . . . . . . 13 ((𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
135134adantl 481 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
136 iunss 4497 . . . . . . . . . . . 12 ( 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢 ↔ ∀𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
137135, 136sylibr 223 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → 𝑥𝐴 (𝐹 “ (𝐵 ∩ ((ℂ ∩ ran 𝑔) ∖ {𝐶}))) ⊆ 𝑢)
138112, 137syl5eqss 3612 . . . . . . . . . 10 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)
139 eleq2 2677 . . . . . . . . . . . 12 (𝑣 = (ℂ ∩ ran 𝑔) → (𝐶𝑣𝐶 ∈ (ℂ ∩ ran 𝑔)))
140 ineq1 3769 . . . . . . . . . . . . . 14 (𝑣 = (ℂ ∩ ran 𝑔) → (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})) = ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶})))
141140imaeq2d 5385 . . . . . . . . . . . . 13 (𝑣 = (ℂ ∩ ran 𝑔) → (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) = (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))))
142141sseq1d 3595 . . . . . . . . . . . 12 (𝑣 = (ℂ ∩ ran 𝑔) → ((𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢 ↔ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
143139, 142anbi12d 743 . . . . . . . . . . 11 (𝑣 = (ℂ ∩ ran 𝑔) → ((𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢) ↔ (𝐶 ∈ (ℂ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
144143rspcev 3282 . . . . . . . . . 10 (((ℂ ∩ ran 𝑔) ∈ (TopOpen‘ℂfld) ∧ (𝐶 ∈ (ℂ ∩ ran 𝑔) ∧ (𝐹 “ ((ℂ ∩ ran 𝑔) ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
14595, 106, 138, 144syl12anc 1316 . . . . . . . . 9 ((((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) ∧ (𝑔:𝐴⟶(TopOpen‘ℂfld) ∧ ∀𝑥𝐴 (𝐶 ∈ (𝑔𝑥) ∧ ((𝐹𝐵) “ ((𝑔𝑥) ∩ (𝐵 ∖ {𝐶}))) ⊆ 𝑢))) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
14680, 145exlimddv 1850 . . . . . . . 8 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ (𝑢 ∈ (TopOpen‘ℂfld) ∧ 𝑦𝑢)) → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢))
147146expr 641 . . . . . . 7 (((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) ∧ 𝑢 ∈ (TopOpen‘ℂfld)) → (𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
148147ralrimiva 2949 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))
14926adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝐹: 𝑥𝐴 𝐵⟶ℂ)
150 iunss 4497 . . . . . . . . 9 ( 𝑥𝐴 𝐵 ⊆ ℂ ↔ ∀𝑥𝐴 𝐵 ⊆ ℂ)
15135, 150sylibr 223 . . . . . . . 8 (𝜑 𝑥𝐴 𝐵 ⊆ ℂ)
152151adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑥𝐴 𝐵 ⊆ ℂ)
153149, 152, 96, 44ellimc2 23447 . . . . . 6 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → (𝑦 ∈ (𝐹 lim 𝐶) ↔ (𝑦 ∈ ℂ ∧ ∀𝑢 ∈ (TopOpen‘ℂfld)(𝑦𝑢 → ∃𝑣 ∈ (TopOpen‘ℂfld)(𝐶𝑣 ∧ (𝐹 “ (𝑣 ∩ ( 𝑥𝐴 𝐵 ∖ {𝐶}))) ⊆ 𝑢)))))
1549, 148, 153mpbir2and 959 . . . . 5 ((𝜑 ∧ (𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶))) → 𝑦 ∈ (𝐹 lim 𝐶))
155154ex 449 . . . 4 (𝜑 → ((𝑦 ∈ ℂ ∧ ∀𝑥𝐴 𝑦 ∈ ((𝐹𝐵) lim 𝐶)) → 𝑦 ∈ (𝐹 lim 𝐶)))
1568, 155syl5bi 231 . . 3 (𝜑 → (𝑦 ∈ (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) → 𝑦 ∈ (𝐹 lim 𝐶)))
157156ssrdv 3574 . 2 (𝜑 → (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)) ⊆ (𝐹 lim 𝐶))
1587, 157eqssd 3585 1 (𝜑 → (𝐹 lim 𝐶) = (ℂ ∩ 𝑥𝐴 ((𝐹𝐵) lim 𝐶)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  ⦋csb 3499   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  {csn 4125  ∩ cint 4410  ∪ ciun 4455  ∩ ciin 4456  ran crn 5039   ↾ cres 5040   “ cima 5041   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  ℂcc 9813  TopOpenctopn 15905  ℂfldccnfld 19567  Topctop 20517   limℂ climc 23432 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-fz 12198  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-plusg 15781  df-mulr 15782  df-starv 15783  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-rest 15906  df-topn 15907  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-cnfld 19568  df-top 20521  df-bases 20522  df-topon 20523  df-topsp 20524  df-cnp 20842  df-xms 21935  df-ms 21936  df-limc 23436 This theorem is referenced by:  limcun  23465
 Copyright terms: Public domain W3C validator