Metamath Proof Explorer

Theorem limcflf

Description: The limit operator can be expressed as a filter limit, from the filter of neighborhoods of B restricted to A \ { B } , to the topology of the complex numbers. (If B is not a limit point of A , then it is still formally a filter limit, but the neighborhood filter is not a proper filter in this case.) (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
limcflf.c ⊢ 𝐶 = ( 𝐴 ∖ { 𝐵 } )
limcflf.l ⊢ 𝐿 = ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 )
Assertion limcflf ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐹 ↾ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 limcflf.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
2 limcflf.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 limcflf.b ⊢ ( 𝜑 → 𝐵 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) )
4 limcflf.k ⊢ 𝐾 = ( TopOpen ‘ ℂfld )
5 limcflf.c ⊢ 𝐶 = ( 𝐴 ∖ { 𝐵 } )
6 limcflf.l ⊢ 𝐿 = ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 )
7 vex ⊢ 𝑡 ∈ V
8 7 inex1 ⊢ ( 𝑡 ∩ 𝐶 ) ∈ V
9 8 rgenw ⊢ ∀ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝑡 ∩ 𝐶 ) ∈ V
10 eqid ⊢ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) = ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) )
11 imaeq2 ⊢ ( 𝑠 = ( 𝑡 ∩ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) = ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑡 ∩ 𝐶 ) ) )
12 inss2 ⊢ ( 𝑡 ∩ 𝐶 ) ⊆ 𝐶
13 resima2 ⊢ ( ( 𝑡 ∩ 𝐶 ) ⊆ 𝐶 → ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑡 ∩ 𝐶 ) ) = ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) )
14 12 13 ax-mp ⊢ ( ( 𝐹 ↾ 𝐶 ) “ ( 𝑡 ∩ 𝐶 ) ) = ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) )
15 11 14 eqtrdi ⊢ ( 𝑠 = ( 𝑡 ∩ 𝐶 ) → ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) = ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) )
16 15 sseq1d ⊢ ( 𝑠 = ( 𝑡 ∩ 𝐶 ) → ( ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) )
17 10 16 rexrnmptw ⊢ ( ∀ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝑡 ∩ 𝐶 ) ∈ V → ( ∃ 𝑠 ∈ ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ↔ ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) )
18 9 17 mp1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ∃ 𝑠 ∈ ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ↔ ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) )
19 fvex ⊢ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∈ V
20 difss ⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴
21 5 20 eqsstri ⊢ 𝐶 ⊆ 𝐴
22 21 2 sstrid ⊢ ( 𝜑 → 𝐶 ⊆ ℂ )
23 cnex ⊢ ℂ ∈ V
24 23 ssex ⊢ ( 𝐶 ⊆ ℂ → 𝐶 ∈ V )
25 22 24 syl ⊢ ( 𝜑 → 𝐶 ∈ V )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → 𝐶 ∈ V )
27 restval ⊢ ( ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∈ V ∧ 𝐶 ∈ V ) → ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 ) = ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) )
28 19 26 27 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↾t 𝐶 ) = ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) )
29 6 28 syl5eq ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → 𝐿 = ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) )
30 29 rexeqdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ↔ ∃ 𝑠 ∈ ran ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↦ ( 𝑡 ∩ 𝐶 ) ) ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) )
31 4 cnfldtop ⊢ 𝐾 ∈ Top
32 opnneip ⊢ ( ( 𝐾 ∈ Top ∧ 𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤 ) → 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) )
33 31 32 mp3an1 ⊢ ( ( 𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤 ) → 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) )
34 id ⊢ ( 𝑡 = 𝑤 → 𝑡 = 𝑤 )
35 5 a1i ⊢ ( 𝑡 = 𝑤 → 𝐶 = ( 𝐴 ∖ { 𝐵 } ) )
36 34 35 ineq12d ⊢ ( 𝑡 = 𝑤 → ( 𝑡 ∩ 𝐶 ) = ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) )
37 36 imaeq2d ⊢ ( 𝑡 = 𝑤 → ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) = ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) )
38 37 sseq1d ⊢ ( 𝑡 = 𝑤 → ( ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
39 38 rspcev ⊢ ( ( 𝑤 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) → ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 )
40 33 39 sylan ⊢ ( ( ( 𝑤 ∈ 𝐾 ∧ 𝐵 ∈ 𝑤 ) ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) → ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 )
41 40 anasss ⊢ ( ( 𝑤 ∈ 𝐾 ∧ ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) → ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 )
42 41 rexlimiva ⊢ ( ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) → ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 )
43 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) )
44 4 cnfldtopon ⊢ 𝐾 ∈ ( TopOn ‘ ℂ )
45 44 toponunii ⊢ ℂ = ∪ 𝐾
46 45 neii1 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ) → 𝑡 ⊆ ℂ )
47 31 43 46 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → 𝑡 ⊆ ℂ )
48 45 ntropn ⊢ ( ( 𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ ) → ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∈ 𝐾 )
49 31 47 48 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∈ 𝐾 )
50 45 lpss ⊢ ( ( 𝐾 ∈ Top ∧ 𝐴 ⊆ ℂ ) → ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ⊆ ℂ )
51 31 2 50 sylancr ⊢ ( 𝜑 → ( ( limPt ‘ 𝐾 ) ‘ 𝐴 ) ⊆ ℂ )
52 51 3 sseldd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
53 52 snssd ⊢ ( 𝜑 → { 𝐵 } ⊆ ℂ )
54 53 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → { 𝐵 } ⊆ ℂ )
55 45 neiint ⊢ ( ( 𝐾 ∈ Top ∧ { 𝐵 } ⊆ ℂ ∧ 𝑡 ⊆ ℂ ) → ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ) )
56 31 54 47 55 mp3an2i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ↔ { 𝐵 } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ) )
57 43 56 mpbid ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → { 𝐵 } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) )
58 52 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → 𝐵 ∈ ℂ )
59 snssg ⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ↔ { 𝐵 } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ) )
60 58 59 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ↔ { 𝐵 } ⊆ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ) )
61 57 60 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) )
62 45 ntrss2 ⊢ ( ( 𝐾 ∈ Top ∧ 𝑡 ⊆ ℂ ) → ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ⊆ 𝑡 )
63 31 47 62 sylancr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ⊆ 𝑡 )
64 ssrin ⊢ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ⊆ 𝑡 → ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ⊆ ( 𝑡 ∩ 𝐶 ) )
65 imass2 ⊢ ( ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ⊆ ( 𝑡 ∩ 𝐶 ) → ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) )
66 63 64 65 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) )
67 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 )
68 66 67 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ 𝑢 )
69 eleq2 ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( 𝐵 ∈ 𝑤 ↔ 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ) )
70 5 ineq2i ⊢ ( 𝑤 ∩ 𝐶 ) = ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) )
71 ineq1 ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( 𝑤 ∩ 𝐶 ) = ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) )
72 70 71 eqtr3id ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) )
73 72 imaeq2d ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) = ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) )
74 73 sseq1d ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ↔ ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ 𝑢 ) )
75 69 74 anbi12d ⊢ ( 𝑤 = ( ( int ‘ 𝐾 ) ‘ 𝑡 ) → ( ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ( 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∧ ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ 𝑢 ) ) )
76 75 rspcev ⊢ ( ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∈ 𝐾 ∧ ( 𝐵 ∈ ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∧ ( 𝐹 “ ( ( ( int ‘ 𝐾 ) ‘ 𝑡 ) ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
77 49 61 68 76 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) ∧ ( 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ∧ ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) ) → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) )
78 77 rexlimdvaa ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) )
79 42 78 impbid2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑡 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝐵 } ) ( 𝐹 “ ( 𝑡 ∩ 𝐶 ) ) ⊆ 𝑢 ) )
80 18 30 79 3bitr4rd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ ( 𝑢 ∈ 𝐾 ∧ 𝑥 ∈ 𝑢 ) ) → ( ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) )
81 80 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) ∧ 𝑥 ∈ 𝑢 ) → ( ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ↔ ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) )
82 81 pm5.74da ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑢 ∈ 𝐾 ) → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) ) )
83 82 ralbidva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ↔ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) ) )
84 83 pm5.32da ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) ) ) )
85 1 2 52 4 ellimc2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑤 ∈ 𝐾 ( 𝐵 ∈ 𝑤 ∧ ( 𝐹 “ ( 𝑤 ∩ ( 𝐴 ∖ { 𝐵 } ) ) ) ⊆ 𝑢 ) ) ) ) )
86 1 2 3 4 5 6 limcflflem ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝐶 ) )
87 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℂ )
88 1 21 87 sylancl ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℂ )
89 isflf ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ℂ ) ∧ 𝐿 ∈ ( Fil ‘ 𝐶 ) ∧ ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ ℂ ) → ( 𝑥 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐹 ↾ 𝐶 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) ) ) )
90 44 86 88 89 mp3an2i ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐹 ↾ 𝐶 ) ) ↔ ( 𝑥 ∈ ℂ ∧ ∀ 𝑢 ∈ 𝐾 ( 𝑥 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( ( 𝐹 ↾ 𝐶 ) “ 𝑠 ) ⊆ 𝑢 ) ) ) )
91 84 85 90 3bitr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 limℂ 𝐵 ) ↔ 𝑥 ∈ ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐹 ↾ 𝐶 ) ) ) )
92 91 eqrdv ⊢ ( 𝜑 → ( 𝐹 limℂ 𝐵 ) = ( ( 𝐾 fLimf 𝐿 ) ‘ ( 𝐹 ↾ 𝐶 ) ) )