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 ‘ 𝐶 ) ) )