Step |
Hyp |
Ref |
Expression |
1 |
|
fbflim.3 |
⊢ 𝐹 = ( 𝑋 filGen 𝐵 ) |
2 |
|
fgcl |
⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐵 ) ∈ ( Fil ‘ 𝑋 ) ) |
3 |
1 2
|
eqeltrid |
⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) ) |
4 |
|
flimopn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) ) |
5 |
3 4
|
sylan2 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) ) |
6 |
|
toponss |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 ) |
7 |
6
|
ad4ant14 |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 ) |
8 |
1
|
eleq2i |
⊢ ( 𝑥 ∈ 𝐹 ↔ 𝑥 ∈ ( 𝑋 filGen 𝐵 ) ) |
9 |
|
elfg |
⊢ ( 𝐵 ∈ ( fBas ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) |
10 |
9
|
ad3antlr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ ( 𝑋 filGen 𝐵 ) ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) |
11 |
8 10
|
syl5bb |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝑥 ⊆ 𝑋 ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) |
12 |
7 11
|
mpbirand |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐹 ↔ ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) |
13 |
12
|
imbi2d |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ↔ ( 𝐴 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) |
14 |
13
|
ralbidva |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) |
15 |
14
|
pm5.32da |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → 𝑥 ∈ 𝐹 ) ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) ) |
16 |
5 15
|
bitrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐵 ∈ ( fBas ‘ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝐽 ( 𝐴 ∈ 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑦 ⊆ 𝑥 ) ) ) ) |