This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem toponsspwpw

Description: The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021)

Ref Expression
Assertion toponsspwpw 
|- ( TopOn ` A ) C_ ~P ~P A

Proof

Step Hyp Ref Expression
1 rabssab 
 |-  { y e. Top | A = U. y } C_ { y | A = U. y }
2 eqcom 
 |-  ( A = U. y <-> U. y = A )
3 2 abbii 
 |-  { y | A = U. y } = { y | U. y = A }
4 1 3 sseqtri 
 |-  { y e. Top | A = U. y } C_ { y | U. y = A }
5 pwpwssunieq 
 |-  { y | U. y = A } C_ ~P ~P A
6 4 5 sstri 
 |-  { y e. Top | A = U. y } C_ ~P ~P A
7 pwexg 
 |-  ( A e. _V -> ~P A e. _V )
8 7 pwexd 
 |-  ( A e. _V -> ~P ~P A e. _V )
9 ssexg 
 |-  ( ( { y e. Top | A = U. y } C_ ~P ~P A /\ ~P ~P A e. _V ) -> { y e. Top | A = U. y } e. _V )
10 6 8 9 sylancr 
 |-  ( A e. _V -> { y e. Top | A = U. y } e. _V )
11 eqeq1 
 |-  ( x = A -> ( x = U. y <-> A = U. y ) )
12 11 rabbidv 
 |-  ( x = A -> { y e. Top | x = U. y } = { y e. Top | A = U. y } )
13 df-topon 
 |-  TopOn = ( x e. _V |-> { y e. Top | x = U. y } )
14 12 13 fvmptg 
 |-  ( ( A e. _V /\ { y e. Top | A = U. y } e. _V ) -> ( TopOn ` A ) = { y e. Top | A = U. y } )
15 10 14 mpdan 
 |-  ( A e. _V -> ( TopOn ` A ) = { y e. Top | A = U. y } )
16 15 6 eqsstrdi 
 |-  ( A e. _V -> ( TopOn ` A ) C_ ~P ~P A )
17 fvprc 
 |-  ( -. A e. _V -> ( TopOn ` A ) = (/) )
18 0ss 
 |-  (/) C_ ~P ~P A
19 17 18 eqsstrdi 
 |-  ( -. A e. _V -> ( TopOn ` A ) C_ ~P ~P A )
20 16 19 pm2.61i 
 |-  ( TopOn ` A ) C_ ~P ~P A