This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgss3

Description: A criterion for determining whether one topology is finer than another. Lemma 2.2 of Munkres p. 80 using abbreviations. (Contributed by NM, 20-Jul-2006) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgss3 ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 bastg ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
2 1 adantr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
3 sstr2 ⊢ ( 𝐵 ⊆ ( topGen ‘ 𝐵 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) → 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )
4 2 3 syl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) → 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )
5 fvex ⊢ ( topGen ‘ 𝐶 ) ∈ V
6 tgss ⊢ ( ( ( topGen ‘ 𝐶 ) ∈ V ∧ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ ( topGen ‘ 𝐶 ) ) )
7 5 6 mpan ⊢ ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ ( topGen ‘ 𝐶 ) ) )
8 tgidm ⊢ ( 𝐶 ∈ 𝑊 → ( topGen ‘ ( topGen ‘ 𝐶 ) ) = ( topGen ‘ 𝐶 ) )
9 8 adantl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( topGen ‘ ( topGen ‘ 𝐶 ) ) = ( topGen ‘ 𝐶 ) )
10 9 sseq2d ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ ( topGen ‘ 𝐶 ) ) ↔ ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ) )
11 7 10 imbitrid ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ) )
12 4 11 impbid ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑊 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )