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 ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ∪ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐶 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) ) ) )