Metamath Proof Explorer

Theorem flffbas

Description: Limit points of a function can be defined using filter bases. (Contributed by Jeff Hankins, 9-Nov-2009) (Revised by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypothesis flffbas.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
Assertion flffbas ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) ) )

Proof

Step Hyp Ref Expression
1 flffbas.l ⊢ 𝐿 = ( 𝑌 filGen 𝐵 )
2 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
3 1 2 eqeltrid ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐿 ∈ ( Fil ‘ 𝑌 ) )
4 isflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) ) ) )
5 3 4 syl3an2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) ) ) )
6 1 eleq2i ⊢ ( 𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ( 𝑌 filGen 𝐵 ) )
7 elfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑡 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
8 7 3ad2ant2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( 𝑌 filGen 𝐵 ) ↔ ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) ) )
9 sstr2 ⊢ ( ( 𝐹 “ 𝑠 ) ⊆ ( 𝐹 “ 𝑡 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
10 imass2 ⊢ ( 𝑠 ⊆ 𝑡 → ( 𝐹 “ 𝑠 ) ⊆ ( 𝐹 “ 𝑡 ) )
11 9 10 syl11 ⊢ ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ( 𝑠 ⊆ 𝑡 → ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
12 11 adantl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) → ( 𝑠 ⊆ 𝑡 → ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
13 12 reximdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) → ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
14 13 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
15 14 com23 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
16 15 adantld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝑡 ⊆ 𝑌 ∧ ∃ 𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
17 8 16 sylbid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝑡 ∈ ( 𝑌 filGen 𝐵 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
18 17 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑡 ∈ ( 𝑌 filGen 𝐵 ) → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
19 6 18 biimtrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑡 ∈ 𝐿 → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
20 19 rexlimdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
21 ssfg ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ ( 𝑌 filGen 𝐵 ) )
22 21 1 sseqtrrdi ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → 𝐵 ⊆ 𝐿 )
23 22 sselda ⊢ ( ( 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ∈ 𝐿 )
24 23 3ad2antl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑠 ∈ 𝐵 ) → 𝑠 ∈ 𝐿 )
25 24 ad2ant2r ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑠 ∈ 𝐵 ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) → 𝑠 ∈ 𝐿 )
26 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑠 ∈ 𝐵 ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) → ( 𝐹 “ 𝑠 ) ⊆ 𝑜 )
27 imaeq2 ⊢ ( 𝑡 = 𝑠 → ( 𝐹 “ 𝑡 ) = ( 𝐹 “ 𝑠 ) )
28 27 sseq1d ⊢ ( 𝑡 = 𝑠 → ( ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ↔ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
29 28 rspcev ⊢ ( ( 𝑠 ∈ 𝐿 ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 )
30 25 26 29 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝑠 ∈ 𝐵 ∧ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 )
31 30 rexlimdvaa ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) )
32 20 31 impbid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ↔ ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
33 32 imbi2d ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 ∈ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) ↔ ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
34 33 ralbidv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) ↔ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
35 34 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑡 ∈ 𝐿 ( 𝐹 “ 𝑡 ) ⊆ 𝑜 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) ) )
36 5 35 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐽 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐵 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) ) )