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) \subseteq 𝒫 𝒫 A$

Step	Hyp	Ref	Expression
1		rabssab	$⊢ \{y \in Top \| A = ⋃ y\} \subseteq \{y \| A = ⋃ y\}$
2		eqcom	$⊢ A = ⋃ y \leftrightarrow ⋃ y = A$
3	2	abbii	$⊢ \{y \| A = ⋃ y\} = \{y \| ⋃ y = A\}$
4	1 3	sseqtri	$⊢ \{y \in Top \| A = ⋃ y\} \subseteq \{y \| ⋃ y = A\}$
5		pwpwssunieq	$⊢ \{y \| ⋃ y = A\} \subseteq 𝒫 𝒫 A$
6	4 5	sstri	$⊢ \{y \in Top \| A = ⋃ y\} \subseteq 𝒫 𝒫 A$
7		pwexg	$⊢ A \in V \to 𝒫 A \in V$
8	7	pwexd	$⊢ A \in V \to 𝒫 𝒫 A \in V$
9		ssexg	$⊢ (\{y \in Top \| A = ⋃ y\} \subseteq 𝒫 𝒫 A \land 𝒫 𝒫 A \in V) \to \{y \in Top \| A = ⋃ y\} \in V$
10	6 8 9	sylancr	$⊢ A \in V \to \{y \in Top \| A = ⋃ y\} \in V$
11		eqeq1	$⊢ x = A \to (x = ⋃ y \leftrightarrow A = ⋃ y)$
12	11	rabbidv	$⊢ x = A \to \{y \in Top \| x = ⋃ y\} = \{y \in Top \| A = ⋃ y\}$
13		df-topon	$⊢ TopOn = (x \in V ⟼ \{y \in Top \| x = ⋃ y\})$
14	12 13	fvmptg	$⊢ (A \in V \land \{y \in Top \| A = ⋃ y\} \in V) \to TopOn (A) = \{y \in Top \| A = ⋃ y\}$
15	10 14	mpdan	$⊢ A \in V \to TopOn (A) = \{y \in Top \| A = ⋃ y\}$
16	15 6	eqsstrdi	$⊢ A \in V \to TopOn (A) \subseteq 𝒫 𝒫 A$
17		fvprc	$⊢ \neg A \in V \to TopOn (A) = \emptyset$
18		0ss	$⊢ \emptyset \subseteq 𝒫 𝒫 A$
19	17 18	eqsstrdi	$⊢ \neg A \in V \to TopOn (A) \subseteq 𝒫 𝒫 A$
20	16 19	pm2.61i	$⊢ TopOn (A) \subseteq 𝒫 𝒫 A$

Metamath Proof Explorer