Metamath Proof Explorer

Theorem flftg

Description: Limit points of a function can be defined using topological bases. (Contributed by Mario Carneiro, 19-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 flftg.l ⊢ 𝐽 = ( topGen ‘ 𝐵 )
2 isflf ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ) ) )
3 1 raleqi ⊢ ( ∀ 𝑢 ∈ 𝐽 ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ↔ ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
4 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
5 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
6 4 5 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ Top )
7 1 6 eqeltrrid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( topGen ‘ 𝐵 ) ∈ Top )
8 tgclb ⊢ ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )
9 7 8 sylibr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐵 ∈ TopBases )
10 bastg ⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
11 eleq2w ⊢ ( 𝑢 = 𝑜 → ( 𝐴 ∈ 𝑢 ↔ 𝐴 ∈ 𝑜 ) )
12 sseq2 ⊢ ( 𝑢 = 𝑜 → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ↔ ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
13 12 rexbidv ⊢ ( 𝑢 = 𝑜 → ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ↔ ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
14 11 13 imbi12d ⊢ ( 𝑢 = 𝑜 → ( ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ↔ ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
15 14 cbvralvw ⊢ ( ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ↔ ∀ 𝑜 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) )
16 ssralv ⊢ ( 𝐵 ⊆ ( topGen ‘ 𝐵 ) → ( ∀ 𝑜 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
17 15 16 syl5bi ⊢ ( 𝐵 ⊆ ( topGen ‘ 𝐵 ) → ( ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) → ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
18 9 10 17 3syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) → ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
19 tg2 ⊢ ( ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) )
20 r19.29 ⊢ ( ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ ∃ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) ) → ∃ 𝑜 ∈ 𝐵 ( ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) ) )
21 simpl ⊢ ( ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → 𝐴 ∈ 𝑜 )
22 simpr ⊢ ( ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → 𝑜 ⊆ 𝑢 )
23 sstr2 ⊢ ( ( 𝐹 “ 𝑠 ) ⊆ 𝑜 → ( 𝑜 ⊆ 𝑢 → ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
24 22 23 syl5com ⊢ ( ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑜 → ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
25 24 reximdv ⊢ ( ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → ( ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
26 21 25 embantd ⊢ ( ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → ( ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
27 26 impcom ⊢ ( ( ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 )
28 27 rexlimivw ⊢ ( ∃ 𝑜 ∈ 𝐵 ( ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 )
29 20 28 syl ⊢ ( ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ ∃ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 )
30 29 ex ⊢ ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ( ∃ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑢 ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
31 19 30 syl5 ⊢ ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ( ( 𝑢 ∈ ( topGen ‘ 𝐵 ) ∧ 𝐴 ∈ 𝑢 ) → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
32 31 expdimp ⊢ ( ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ∧ 𝑢 ∈ ( topGen ‘ 𝐵 ) ) → ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
33 32 ralrimiva ⊢ ( ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) → ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) )
34 18 33 impbid1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑢 ∈ ( topGen ‘ 𝐵 ) ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ↔ ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
35 3 34 syl5bb ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ↔ ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) )
36 35 pm5.32da ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐴 ∈ 𝑢 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑢 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) ) )
37 2 36 bitrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐿 ∈ ( Fil ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) → ( 𝐴 ∈ ( ( 𝐽 fLimf 𝐿 ) ‘ 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑜 ∈ 𝐵 ( 𝐴 ∈ 𝑜 → ∃ 𝑠 ∈ 𝐿 ( 𝐹 “ 𝑠 ) ⊆ 𝑜 ) ) ) )