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