Metamath Proof Explorer


Theorem eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion eltg2b ( 𝐵𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eltg2 ( 𝐵𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ( 𝐴 𝐵 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) ) ) )
2 simpl ( ( 𝑥𝑦𝑦𝐴 ) → 𝑥𝑦 )
3 2 reximi ( ∃ 𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) → ∃ 𝑦𝐵 𝑥𝑦 )
4 eluni2 ( 𝑥 𝐵 ↔ ∃ 𝑦𝐵 𝑥𝑦 )
5 3 4 sylibr ( ∃ 𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) → 𝑥 𝐵 )
6 5 ralimi ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) → ∀ 𝑥𝐴 𝑥 𝐵 )
7 dfss3 ( 𝐴 𝐵 ↔ ∀ 𝑥𝐴 𝑥 𝐵 )
8 6 7 sylibr ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) → 𝐴 𝐵 )
9 8 pm4.71ri ( ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) ↔ ( 𝐴 𝐵 ∧ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) ) )
10 1 9 bitr4di ( 𝐵𝑉 → ( 𝐴 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐴𝑦𝐵 ( 𝑥𝑦𝑦𝐴 ) ) )