Metamath Proof Explorer


Theorem basgen2

Description: Given a topology J , show that a subset B satisfying the third antecedent is a basis for it. Lemma 2.3 of Munkres p. 81. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion basgen2 ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ∧ ∀ 𝑥𝐽𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )

Proof

Step Hyp Ref Expression
1 dfss3 ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) )
2 ssexg ( ( 𝐵𝐽𝐽 ∈ Top ) → 𝐵 ∈ V )
3 2 ancoms ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → 𝐵 ∈ V )
4 eltg2b ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
5 3 4 syl ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
6 5 ralbidv ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( ∀ 𝑥𝐽 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐽𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
7 1 6 syl5bb ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ) → ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥𝐽𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) )
8 7 biimp3ar ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ∧ ∀ 𝑥𝐽𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) → 𝐽 ⊆ ( topGen ‘ 𝐵 ) )
9 basgen ( ( 𝐽 ∈ Top ∧ 𝐵𝐽𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )
10 8 9 syld3an3 ( ( 𝐽 ∈ Top ∧ 𝐵𝐽 ∧ ∀ 𝑥𝐽𝑦𝑥𝑧𝐵 ( 𝑦𝑧𝑧𝑥 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )