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 ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) ≼ 𝒫 𝐵 )

Proof

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