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 ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		rabssab	⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ { 𝑦 ∣ 𝐴 = ∪ 𝑦 }
2		eqcom	⊢ ( 𝐴 = ∪ 𝑦 ↔ ∪ 𝑦 = 𝐴 )
3	2	abbii	⊢ { 𝑦 ∣ 𝐴 = ∪ 𝑦 } = { 𝑦 ∣ ∪ 𝑦 = 𝐴 }
4	1 3	sseqtri	⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ { 𝑦 ∣ ∪ 𝑦 = 𝐴 }
5		pwpwssunieq	⊢ { 𝑦 ∣ ∪ 𝑦 = 𝐴 } ⊆ 𝒫 𝒫 𝐴
6	4 5	sstri	⊢ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ 𝒫 𝒫 𝐴
7		pwexg	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
8	7	pwexd	⊢ ( 𝐴 ∈ V → 𝒫 𝒫 𝐴 ∈ V )
9		ssexg	⊢ ( ( { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ⊆ 𝒫 𝒫 𝐴 ∧ 𝒫 𝒫 𝐴 ∈ V ) → { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V )
10	6 8 9	sylancr	⊢ ( 𝐴 ∈ V → { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V )
11		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∪ 𝑦 ↔ 𝐴 = ∪ 𝑦 ) )
12	11	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } )
13		df-topon	⊢ TopOn = ( 𝑥 ∈ V ↦ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } )
14	12 13	fvmptg	⊢ ( ( 𝐴 ∈ V ∧ { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } ∈ V ) → ( TopOn ‘ 𝐴 ) = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } )
15	10 14	mpdan	⊢ ( 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) = { 𝑦 ∈ Top ∣ 𝐴 = ∪ 𝑦 } )
16	15 6	eqsstrdi	⊢ ( 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴 )
17		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) = ∅ )
18		0ss	⊢ ∅ ⊆ 𝒫 𝒫 𝐴
19	17 18	eqsstrdi	⊢ ( ¬ 𝐴 ∈ V → ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴 )
20	16 19	pm2.61i	⊢ ( TopOn ‘ 𝐴 ) ⊆ 𝒫 𝒫 𝐴