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 ⊢B∈V∧⋃B=⋃C→topGen⁡B⊆topGen⁡C↔∀x∈⋃B∀y∈Bx∈y→∃z∈Cx∈z∧z⊆y

Proof

Step Hyp Ref Expression
1 simpr ⊢B∈V∧⋃B=⋃C→⋃B=⋃C
2 uniexg ⊢B∈V→⋃B∈V
3 2 adantr ⊢B∈V∧⋃B=⋃C→⋃B∈V
4 1 3 eqeltrrd ⊢B∈V∧⋃B=⋃C→⋃C∈V
5 uniexb ⊢C∈V↔⋃C∈V
6 4 5 sylibr ⊢B∈V∧⋃B=⋃C→C∈V
7 tgss3 ⊢B∈V∧C∈V→topGen⁡B⊆topGen⁡C↔B⊆topGen⁡C
8 6 7 syldan ⊢B∈V∧⋃B=⋃C→topGen⁡B⊆topGen⁡C↔B⊆topGen⁡C
9 eltg2b ⊢C∈V→y∈topGen⁡C↔∀x∈y∃z∈Cx∈z∧z⊆y
10 6 9 syl ⊢B∈V∧⋃B=⋃C→y∈topGen⁡C↔∀x∈y∃z∈Cx∈z∧z⊆y
11 elunii ⊢x∈y∧y∈B→x∈⋃B
12 11 ancoms ⊢y∈B∧x∈y→x∈⋃B
13 biimt ⊢x∈⋃B→∃z∈Cx∈z∧z⊆y↔x∈⋃B→∃z∈Cx∈z∧z⊆y
14 12 13 syl ⊢y∈B∧x∈y→∃z∈Cx∈z∧z⊆y↔x∈⋃B→∃z∈Cx∈z∧z⊆y
15 14 ralbidva ⊢y∈B→∀x∈y∃z∈Cx∈z∧z⊆y↔∀x∈yx∈⋃B→∃z∈Cx∈z∧z⊆y
16 10 15 sylan9bb ⊢B∈V∧⋃B=⋃C∧y∈B→y∈topGen⁡C↔∀x∈yx∈⋃B→∃z∈Cx∈z∧z⊆y
17 ralcom3 ⊢∀x∈yx∈⋃B→∃z∈Cx∈z∧z⊆y↔∀x∈⋃Bx∈y→∃z∈Cx∈z∧z⊆y
18 16 17 bitrdi ⊢B∈V∧⋃B=⋃C∧y∈B→y∈topGen⁡C↔∀x∈⋃Bx∈y→∃z∈Cx∈z∧z⊆y
19 18 ralbidva ⊢B∈V∧⋃B=⋃C→∀y∈By∈topGen⁡C↔∀y∈B∀x∈⋃Bx∈y→∃z∈Cx∈z∧z⊆y
20 dfss3 ⊢B⊆topGen⁡C↔∀y∈By∈topGen⁡C
21 ralcom ⊢∀x∈⋃B∀y∈Bx∈y→∃z∈Cx∈z∧z⊆y↔∀y∈B∀x∈⋃Bx∈y→∃z∈Cx∈z∧z⊆y
22 19 20 21 3bitr4g ⊢B∈V∧⋃B=⋃C→B⊆topGen⁡C↔∀x∈⋃B∀y∈Bx∈y→∃z∈Cx∈z∧z⊆y
23 8 22 bitrd ⊢B∈V∧⋃B=⋃C→topGen⁡B⊆topGen⁡C↔∀x∈⋃B∀y∈Bx∈y→∃z∈Cx∈z∧z⊆y