dmtopon

Description: The domain of TopOn is the universal class _V . (Contributed by BJ, 29-Apr-2021)

		Ref	Expression
	Assertion	dmtopon	$⊢ dom TopOn = V$

Step	Hyp	Ref	Expression
1		vpwex	$⊢ 𝒫 x \in V$
2	1	pwex	$⊢ 𝒫 𝒫 x \in V$
3		eqcom	$⊢ x = ⋃ y \leftrightarrow ⋃ y = x$
4	3	rabbii	$⊢ \{y \in Top \| x = ⋃ y\} = \{y \in Top \| ⋃ y = x\}$
5		rabssab	$⊢ \{y \in Top \| ⋃ y = x\} \subseteq \{y \| ⋃ y = x\}$
6		pwpwssunieq	$⊢ \{y \| ⋃ y = x\} \subseteq 𝒫 𝒫 x$
7	5 6	sstri	$⊢ \{y \in Top \| ⋃ y = x\} \subseteq 𝒫 𝒫 x$
8	4 7	eqsstri	$⊢ \{y \in Top \| x = ⋃ y\} \subseteq 𝒫 𝒫 x$
9	2 8	ssexi	$⊢ \{y \in Top \| x = ⋃ y\} \in V$
10		df-topon	$⊢ TopOn = (x \in V ⟼ \{y \in Top \| x = ⋃ y\})$
11	9 10	dmmpti	$⊢ dom TopOn = V$

Metamath Proof Explorer