Metamath Proof Explorer


Theorem tgss2

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

Ref Expression
Assertion tgss2 ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 𝐵𝑦𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐵𝑉 𝐵 = 𝐶 ) → 𝐵 = 𝐶 )
2 uniexg ( 𝐵𝑉 𝐵 ∈ V )
3 2 adantr ( ( 𝐵𝑉 𝐵 = 𝐶 ) → 𝐵 ∈ V )
4 1 3 eqeltrrd ( ( 𝐵𝑉 𝐵 = 𝐶 ) → 𝐶 ∈ V )
5 uniexb ( 𝐶 ∈ V ↔ 𝐶 ∈ V )
6 4 5 sylibr ( ( 𝐵𝑉 𝐵 = 𝐶 ) → 𝐶 ∈ V )
7 tgss3 ( ( 𝐵𝑉𝐶 ∈ V ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )
8 6 7 syldan ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ 𝐵 ⊆ ( topGen ‘ 𝐶 ) ) )
9 eltg2b ( 𝐶 ∈ V → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥𝑦𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) )
10 6 9 syl ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥𝑦𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) )
11 elunii ( ( 𝑥𝑦𝑦𝐵 ) → 𝑥 𝐵 )
12 11 ancoms ( ( 𝑦𝐵𝑥𝑦 ) → 𝑥 𝐵 )
13 biimt ( 𝑥 𝐵 → ( ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ↔ ( 𝑥 𝐵 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
14 12 13 syl ( ( 𝑦𝐵𝑥𝑦 ) → ( ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ↔ ( 𝑥 𝐵 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
15 14 ralbidva ( 𝑦𝐵 → ( ∀ 𝑥𝑦𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ↔ ∀ 𝑥𝑦 ( 𝑥 𝐵 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
16 10 15 sylan9bb ( ( ( 𝐵𝑉 𝐵 = 𝐶 ) ∧ 𝑦𝐵 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥𝑦 ( 𝑥 𝐵 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
17 ralcom3 ( ∀ 𝑥𝑦 ( 𝑥 𝐵 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ↔ ∀ 𝑥 𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) )
18 16 17 bitrdi ( ( ( 𝐵𝑉 𝐵 = 𝐶 ) ∧ 𝑦𝐵 ) → ( 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
19 18 ralbidva ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( ∀ 𝑦𝐵 𝑦 ∈ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑦𝐵𝑥 𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
20 dfss3 ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑦𝐵 𝑦 ∈ ( topGen ‘ 𝐶 ) )
21 ralcom ( ∀ 𝑥 𝐵𝑦𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ↔ ∀ 𝑦𝐵𝑥 𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) )
22 19 20 21 3bitr4g ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( 𝐵 ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 𝐵𝑦𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )
23 8 22 bitrd ( ( 𝐵𝑉 𝐵 = 𝐶 ) → ( ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ 𝐶 ) ↔ ∀ 𝑥 𝐵𝑦𝐵 ( 𝑥𝑦 → ∃ 𝑧𝐶 ( 𝑥𝑧𝑧𝑦 ) ) ) )