Metamath Proof Explorer

Theorem limciun

Description: A point is a limit of F on the finite union U_ x e. A B ( x ) iff it is the limit of the restriction of F to each B ( x ) . (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Hypotheses limciun.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
limciun.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
limciun.3 ⊢ ( 𝜑 → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ℂ )
limciun.4 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion limciun ( 𝜑 → ( 𝐹 limℂ 𝐶 ) = ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 limciun.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 limciun.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
3 limciun.3 ⊢ ( 𝜑 → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ℂ )
4 limciun.4 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
5 limccl ⊢ ( 𝐹 limℂ 𝐶 ) ⊆ ℂ
6 limcresi ⊢ ( 𝐹 limℂ 𝐶 ) ⊆ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 )
7 6 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐹 limℂ 𝐶 ) ⊆ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 )
8 ssiin ⊢ ( ( 𝐹 limℂ 𝐶 ) ⊆ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 limℂ 𝐶 ) ⊆ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) )
9 7 8 mpbir ⊢ ( 𝐹 limℂ 𝐶 ) ⊆ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 )
10 5 9 ssini ⊢ ( 𝐹 limℂ 𝐶 ) ⊆ ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) )
11 10 a1i ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐶 ) ⊆ ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) )
12 elriin ⊢ ( 𝑦 ∈ ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ↔ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) )
13 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → 𝑦 ∈ ℂ )
14 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → 𝐴 ∈ Fin )
15 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) )
16 nfcv ⊢ Ⅎ 𝑥 𝐹
17 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵
18 16 17 nfres ⊢ Ⅎ 𝑥 ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
19 nfcv ⊢ Ⅎ 𝑥 limℂ
20 nfcv ⊢ Ⅎ 𝑥 𝐶
21 18 19 20 nfov ⊢ Ⅎ 𝑥 ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 )
22 21 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 )
23 csbeq1a ⊢ ( 𝑥 = 𝑎 → 𝐵 = ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
24 23 reseq2d ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ↾ 𝐵 ) = ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) )
25 24 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) = ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) )
26 25 eleq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ↔ 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) ) )
27 22 26 rspc ⊢ ( 𝑎 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) → 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) ) )
28 15 27 mpan9 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) )
29 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ℂ )
30 ssiun2 ⊢ ( 𝑎 ∈ 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ∪ 𝑎 ∈ 𝐴 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 )
31 nfcv ⊢ Ⅎ 𝑎 𝐵
32 31 17 23 cbviun ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑎 ∈ 𝐴 ⦋ 𝑎 / 𝑥 ⦌ 𝐵
33 30 32 sseqtrrdi ⊢ ( 𝑎 ∈ 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
34 33 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
35 29 34 fssresd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) : ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⟶ ℂ )
36 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
37 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
38 nfcv ⊢ Ⅎ 𝑥 ℂ
39 17 38 nfss ⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ℂ
40 23 sseq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐵 ⊆ ℂ ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ℂ ) )
41 39 40 rspc ⊢ ( 𝑎 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ℂ ) )
42 36 37 41 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ⊆ ℂ )
43 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
44 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
45 35 42 43 44 ellimc2 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) ↔ ( 𝑦 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) ) )
46 45 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑦 ∈ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) limℂ 𝐶 ) ↔ ( 𝑦 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) ) )
47 28 46 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → ( 𝑦 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) )
48 47 simprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
49 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑢 ∈ ( TopOpen ‘ ℂfld ) )
50 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → 𝑦 ∈ 𝑢 )
51 rsp ⊢ ( ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) → ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) → ( 𝑦 ∈ 𝑢 → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) )
52 48 49 50 51 syl3c ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ 𝑎 ∈ 𝐴 ) → ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
53 52 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → ∀ 𝑎 ∈ 𝐴 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
54 nfv ⊢ Ⅎ 𝑎 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
55 nfcv ⊢ Ⅎ 𝑥 ( TopOpen ‘ ℂfld )
56 nfv ⊢ Ⅎ 𝑥 𝐶 ∈ 𝑘
57 nfcv ⊢ Ⅎ 𝑥 𝑘
58 nfcv ⊢ Ⅎ 𝑥 { 𝐶 }
59 17 58 nfdif ⊢ Ⅎ 𝑥 ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } )
60 57 59 nfin ⊢ Ⅎ 𝑥 ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) )
61 18 60 nfima ⊢ Ⅎ 𝑥 ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) )
62 nfcv ⊢ Ⅎ 𝑥 𝑢
63 61 62 nfss ⊢ Ⅎ 𝑥 ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢
64 56 63 nfan ⊢ Ⅎ 𝑥 ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
65 55 64 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
66 23 difeq1d ⊢ ( 𝑥 = 𝑎 → ( 𝐵 ∖ { 𝐶 } ) = ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) )
67 66 ineq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) = ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) )
68 24 67 imaeq12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) = ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) )
69 68 sseq1d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ↔ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
70 69 anbi2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
71 70 rexbidv ⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
72 54 65 71 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ↔ ∀ 𝑎 ∈ 𝐴 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ) “ ( 𝑘 ∩ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
73 53 72 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → ∀ 𝑥 ∈ 𝐴 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
74 eleq2 ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( 𝐶 ∈ 𝑘 ↔ 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ) )
75 ineq1 ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) = ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) )
76 75 imaeq2d ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) = ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) )
77 76 sseq1d ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ↔ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
78 74 77 anbi12d ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
79 78 ac6sfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑘 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑘 ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝑘 ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
80 14 73 79 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → ∃ 𝑔 ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
81 44 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
82 frn ⊢ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) → ran 𝑔 ⊆ ( TopOpen ‘ ℂfld ) )
83 82 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ran 𝑔 ⊆ ( TopOpen ‘ ℂfld ) )
84 14 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → 𝐴 ∈ Fin )
85 ffn ⊢ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) → 𝑔 Fn 𝐴 )
86 85 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → 𝑔 Fn 𝐴 )
87 dffn4 ⊢ ( 𝑔 Fn 𝐴 ↔ 𝑔 : 𝐴 –onto→ ran 𝑔 )
88 86 87 sylib ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → 𝑔 : 𝐴 –onto→ ran 𝑔 )
89 fofi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑔 : 𝐴 –onto→ ran 𝑔 ) → ran 𝑔 ∈ Fin )
90 84 88 89 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ran 𝑔 ∈ Fin )
91 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
92 91 rintopn ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ran 𝑔 ⊆ ( TopOpen ‘ ℂfld ) ∧ ran 𝑔 ∈ Fin ) → ( ℂ ∩ ∩ ran 𝑔 ) ∈ ( TopOpen ‘ ℂfld ) )
93 81 83 90 92 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ( ℂ ∩ ∩ ran 𝑔 ) ∈ ( TopOpen ‘ ℂfld ) )
94 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → 𝐶 ∈ ℂ )
95 94 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → 𝐶 ∈ ℂ )
96 simpl ⊢ ( ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) → 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) )
97 96 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) )
98 97 ad2antll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) )
99 eleq2 ⊢ ( 𝑧 = ( 𝑔 ‘ 𝑥 ) → ( 𝐶 ∈ 𝑧 ↔ 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ) )
100 99 ralrn ⊢ ( 𝑔 Fn 𝐴 → ( ∀ 𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ) )
101 86 100 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ( ∀ 𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ) )
102 98 101 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ∀ 𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 )
103 elrint ⊢ ( 𝐶 ∈ ( ℂ ∩ ∩ ran 𝑔 ) ↔ ( 𝐶 ∈ ℂ ∧ ∀ 𝑧 ∈ ran 𝑔 𝐶 ∈ 𝑧 ) )
104 95 102 103 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → 𝐶 ∈ ( ℂ ∩ ∩ ran 𝑔 ) )
105 indifcom ⊢ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) )
106 iunin1 ⊢ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) = ( ∪ 𝑥 ∈ 𝐴 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) )
107 105 106 eqtr4i ⊢ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) = ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) )
108 107 imaeq2i ⊢ ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) = ( 𝐹 “ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) )
109 imaiun ⊢ ( 𝐹 “ ∪ 𝑥 ∈ 𝐴 ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) = ∪ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) )
110 108 109 eqtri ⊢ ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) = ∪ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) )
111 inss2 ⊢ ( ℂ ∩ ∩ ran 𝑔 ) ⊆ ∩ ran 𝑔
112 fnfvelrn ⊢ ( ( 𝑔 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
113 85 112 sylan ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 )
114 intss1 ⊢ ( ( 𝑔 ‘ 𝑥 ) ∈ ran 𝑔 → ∩ ran 𝑔 ⊆ ( 𝑔 ‘ 𝑥 ) )
115 113 114 syl ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ∩ ran 𝑔 ⊆ ( 𝑔 ‘ 𝑥 ) )
116 111 115 sstrid ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( ℂ ∩ ∩ ran 𝑔 ) ⊆ ( 𝑔 ‘ 𝑥 ) )
117 116 ssdifd ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ⊆ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) )
118 sslin ⊢ ( ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ⊆ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) → ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ⊆ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) )
119 imass2 ⊢ ( ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ⊆ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ ( 𝐹 “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ) )
120 117 118 119 3syl ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ ( 𝐹 “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ) )
121 indifcom ⊢ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) = ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) )
122 121 imaeq2i ⊢ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) = ( ( 𝐹 ↾ 𝐵 ) “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) )
123 inss1 ⊢ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ⊆ 𝐵
124 resima2 ⊢ ( ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ) = ( 𝐹 “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ) )
125 123 124 ax-mp ⊢ ( ( 𝐹 ↾ 𝐵 ) “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) ) = ( 𝐹 “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) )
126 122 125 eqtri ⊢ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) = ( 𝐹 “ ( 𝐵 ∩ ( ( 𝑔 ‘ 𝑥 ) ∖ { 𝐶 } ) ) )
127 120 126 sseqtrrdi ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) )
128 sstr2 ⊢ ( ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) → ( ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
129 127 128 syl ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
130 129 adantld ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) → ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
131 130 ralimdva ⊢ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
132 131 imp ⊢ ( ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
133 132 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
134 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
135 133 134 sylibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ∪ 𝑥 ∈ 𝐴 ( 𝐹 “ ( 𝐵 ∩ ( ( ℂ ∩ ∩ ran 𝑔 ) ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
136 110 135 eqsstrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 )
137 eleq2 ⊢ ( 𝑣 = ( ℂ ∩ ∩ ran 𝑔 ) → ( 𝐶 ∈ 𝑣 ↔ 𝐶 ∈ ( ℂ ∩ ∩ ran 𝑔 ) ) )
138 ineq1 ⊢ ( 𝑣 = ( ℂ ∩ ∩ ran 𝑔 ) → ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) = ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) )
139 138 imaeq2d ⊢ ( 𝑣 = ( ℂ ∩ ∩ ran 𝑔 ) → ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) = ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) )
140 139 sseq1d ⊢ ( 𝑣 = ( ℂ ∩ ∩ ran 𝑔 ) → ( ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
141 137 140 anbi12d ⊢ ( 𝑣 = ( ℂ ∩ ∩ ran 𝑔 ) → ( ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐶 ∈ ( ℂ ∩ ∩ ran 𝑔 ) ∧ ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
142 141 rspcev ⊢ ( ( ( ℂ ∩ ∩ ran 𝑔 ) ∈ ( TopOpen ‘ ℂfld ) ∧ ( 𝐶 ∈ ( ℂ ∩ ∩ ran 𝑔 ) ∧ ( 𝐹 “ ( ( ℂ ∩ ∩ ran 𝑔 ) ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
143 93 104 136 142 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) ∧ ( 𝑔 : 𝐴 ⟶ ( TopOpen ‘ ℂfld ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ∈ ( 𝑔 ‘ 𝑥 ) ∧ ( ( 𝐹 ↾ 𝐵 ) “ ( ( 𝑔 ‘ 𝑥 ) ∩ ( 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
144 80 143 exlimddv ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ ( 𝑢 ∈ ( TopOpen ‘ ℂfld ) ∧ 𝑦 ∈ 𝑢 ) ) → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) )
145 144 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) ∧ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ) → ( 𝑦 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
146 145 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) )
147 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → 𝐹 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ℂ )
148 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
149 2 148 sylibr ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
150 149 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ℂ )
151 147 150 94 44 ellimc2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → ( 𝑦 ∈ ( 𝐹 limℂ 𝐶 ) ↔ ( 𝑦 ∈ ℂ ∧ ∀ 𝑢 ∈ ( TopOpen ‘ ℂfld ) ( 𝑦 ∈ 𝑢 → ∃ 𝑣 ∈ ( TopOpen ‘ ℂfld ) ( 𝐶 ∈ 𝑣 ∧ ( 𝐹 “ ( 𝑣 ∩ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∖ { 𝐶 } ) ) ) ⊆ 𝑢 ) ) ) ) )
152 13 146 151 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ) → 𝑦 ∈ ( 𝐹 limℂ 𝐶 ) )
153 152 ex ⊢ ( 𝜑 → ( ( 𝑦 ∈ ℂ ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) → 𝑦 ∈ ( 𝐹 limℂ 𝐶 ) ) )
154 12 153 biimtrid ⊢ ( 𝜑 → ( 𝑦 ∈ ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) → 𝑦 ∈ ( 𝐹 limℂ 𝐶 ) ) )
155 154 ssrdv ⊢ ( 𝜑 → ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) ⊆ ( 𝐹 limℂ 𝐶 ) )
156 11 155 eqssd ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐶 ) = ( ℂ ∩ ∩ 𝑥 ∈ 𝐴 ( ( 𝐹 ↾ 𝐵 ) limℂ 𝐶 ) ) )