Theorem dmtopon

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

	Ref	Expression
Assertion	dmtopon	⊢ dom TopOn = V

Proof

Step	Hyp	Ref	Expression
1		vpwex	⊢ 𝒫 𝑥 ∈ V
2	1	pwex	⊢ 𝒫 𝒫 𝑥 ∈ V
3		eqcom	⊢ ( 𝑥 = ∪ 𝑦 ↔ ∪ 𝑦 = 𝑥 )
4	3	rabbii	⊢ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } = { 𝑦 ∈ Top ∣ ∪ 𝑦 = 𝑥 }
5		rabssab	⊢ { 𝑦 ∈ Top ∣ ∪ 𝑦 = 𝑥 } ⊆ { 𝑦 ∣ ∪ 𝑦 = 𝑥 }
6		pwpwssunieq	⊢ { 𝑦 ∣ ∪ 𝑦 = 𝑥 } ⊆ 𝒫 𝒫 𝑥
7	5 6	sstri	⊢ { 𝑦 ∈ Top ∣ ∪ 𝑦 = 𝑥 } ⊆ 𝒫 𝒫 𝑥
8	4 7	eqsstri	⊢ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } ⊆ 𝒫 𝒫 𝑥
9	2 8	ssexi	⊢ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } ∈ V
10		df-topon	⊢ TopOn = ( 𝑥 ∈ V ↦ { 𝑦 ∈ Top ∣ 𝑥 = ∪ 𝑦 } )
11	9 10	dmmpti	⊢ dom TopOn = V