Theorem tgss

Description: Subset relation for generated topologies. (Contributed by NM, 7-May-2007)

	Ref	Expression
Assertion	tgss	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ssrin	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( 𝐶 ∩ 𝒫 𝑥 ) )
2	1	unissd	⊢ ( 𝐵 ⊆ 𝐶 → ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) )
3		sstr2	⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → ( ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
4	2 3	syl5com	⊢ ( 𝐵 ⊆ 𝐶 → ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
5	4	adantl	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
6		ssexg	⊢ ( ( 𝐵 ⊆ 𝐶 ∧ 𝐶 ∈ 𝑉 ) → 𝐵 ∈ V )
7	6	ancoms	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → 𝐵 ∈ V )
8		eltg	⊢ ( 𝐵 ∈ V → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
9	7 8	syl	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
10		eltg	⊢ ( 𝐶 ∈ 𝑉 → ( 𝑥 ∈ ( topGen ‘ 𝐶 ) ↔ 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
11	10	adantr	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐶 ) ↔ 𝑥 ⊆ ∪ ( 𝐶 ∩ 𝒫 𝑥 ) ) )
12	5 9 11	3imtr4d	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) → 𝑥 ∈ ( topGen ‘ 𝐶 ) ) )
13	12	ssrdv	⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐶 ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) )