Metamath Proof Explorer

Theorem tgdom

Description: A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015) (Revised by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion tgdom ⊢ B ∈ V → topGen ⁡ B ≼ 𝒫 B

Proof

Step Hyp Ref Expression
1 pwexg ⊢ B ∈ V → 𝒫 B ∈ V
2 inss1 ⊢ B ∩ 𝒫 x ⊆ B
3 vpwex ⊢ 𝒫 x ∈ V
4 3 inex2 ⊢ B ∩ 𝒫 x ∈ V
5 4 elpw ⊢ B ∩ 𝒫 x ∈ 𝒫 B ↔ B ∩ 𝒫 x ⊆ B
6 2 5 mpbir ⊢ B ∩ 𝒫 x ∈ 𝒫 B
7 6 a1i ⊢ x ∈ topGen ⁡ B → B ∩ 𝒫 x ∈ 𝒫 B
8 unieq ⊢ B ∩ 𝒫 x = B ∩ 𝒫 y → ⋃ B ∩ 𝒫 x = ⋃ B ∩ 𝒫 y
9 8 adantl ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B ∧ B ∩ 𝒫 x = B ∩ 𝒫 y → ⋃ B ∩ 𝒫 x = ⋃ B ∩ 𝒫 y
10 eltg4i ⊢ x ∈ topGen ⁡ B → x = ⋃ B ∩ 𝒫 x
11 10 ad2antrr ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B ∧ B ∩ 𝒫 x = B ∩ 𝒫 y → x = ⋃ B ∩ 𝒫 x
12 eltg4i ⊢ y ∈ topGen ⁡ B → y = ⋃ B ∩ 𝒫 y
13 12 ad2antlr ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B ∧ B ∩ 𝒫 x = B ∩ 𝒫 y → y = ⋃ B ∩ 𝒫 y
14 9 11 13 3eqtr4d ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B ∧ B ∩ 𝒫 x = B ∩ 𝒫 y → x = y
15 14 ex ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B → B ∩ 𝒫 x = B ∩ 𝒫 y → x = y
16 pweq ⊢ x = y → 𝒫 x = 𝒫 y
17 16 ineq2d ⊢ x = y → B ∩ 𝒫 x = B ∩ 𝒫 y
18 15 17 impbid1 ⊢ x ∈ topGen ⁡ B ∧ y ∈ topGen ⁡ B → B ∩ 𝒫 x = B ∩ 𝒫 y ↔ x = y
19 7 18 dom2 ⊢ 𝒫 B ∈ V → topGen ⁡ B ≼ 𝒫 B
20 1 19 syl ⊢ B ∈ V → topGen ⁡ B ≼ 𝒫 B