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	bitrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ) → ( 𝐽 ⊆ ( topGen ‘ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) )
8	7	biimp3ar	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → 𝐽 ⊆ ( topGen ‘ 𝐵 ) )
9		basgen	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ 𝐽 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )
10	8 9	syld3an3	⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ 𝐽 ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝐵 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥 ) ) → ( topGen ‘ 𝐵 ) = 𝐽 )