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 e. V -> ( topGen ` B ) ~<_ ~P B )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( B e. V -> ~P B e. _V )
2 inss1 
 |-  ( B i^i ~P x ) C_ B
3 vpwex 
 |-  ~P x e. _V
4 3 inex2 
 |-  ( B i^i ~P x ) e. _V
5 4 elpw 
 |-  ( ( B i^i ~P x ) e. ~P B <-> ( B i^i ~P x ) C_ B )
6 2 5 mpbir 
 |-  ( B i^i ~P x ) e. ~P B
7 6 a1i 
 |-  ( x e. ( topGen ` B ) -> ( B i^i ~P x ) e. ~P B )
8 unieq 
 |-  ( ( B i^i ~P x ) = ( B i^i ~P y ) -> U. ( B i^i ~P x ) = U. ( B i^i ~P y ) )
9 8 adantl 
 |-  ( ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) /\ ( B i^i ~P x ) = ( B i^i ~P y ) ) -> U. ( B i^i ~P x ) = U. ( B i^i ~P y ) )
10 eltg4i 
 |-  ( x e. ( topGen ` B ) -> x = U. ( B i^i ~P x ) )
11 10 ad2antrr 
 |-  ( ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) /\ ( B i^i ~P x ) = ( B i^i ~P y ) ) -> x = U. ( B i^i ~P x ) )
12 eltg4i 
 |-  ( y e. ( topGen ` B ) -> y = U. ( B i^i ~P y ) )
13 12 ad2antlr 
 |-  ( ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) /\ ( B i^i ~P x ) = ( B i^i ~P y ) ) -> y = U. ( B i^i ~P y ) )
14 9 11 13 3eqtr4d 
 |-  ( ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) /\ ( B i^i ~P x ) = ( B i^i ~P y ) ) -> x = y )
15 14 ex 
 |-  ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) -> ( ( B i^i ~P x ) = ( B i^i ~P y ) -> x = y ) )
16 pweq 
 |-  ( x = y -> ~P x = ~P y )
17 16 ineq2d 
 |-  ( x = y -> ( B i^i ~P x ) = ( B i^i ~P y ) )
18 15 17 impbid1 
 |-  ( ( x e. ( topGen ` B ) /\ y e. ( topGen ` B ) ) -> ( ( B i^i ~P x ) = ( B i^i ~P y ) <-> x = y ) )
19 7 18 dom2 
 |-  ( ~P B e. _V -> ( topGen ` B ) ~<_ ~P B )
20 1 19 syl 
 |-  ( B e. V -> ( topGen ` B ) ~<_ ~P B )