df-topgen

Description: Define a function that converts a basis to its corresponding topology. Equivalent to the definition of a topology generated by a basis in Munkres p. 78 (see tgval2 ). The first use of this definition is tgval but the token is used in df-pt . See tgval3 for an alternate expression for the value. (Contributed by NM, 16-Jul-2006)

		Ref	Expression
	Assertion	df-topgen	⊢ topGen = ( 𝑥 ∈ V ↦ { 𝑦 ∣ 𝑦 ⊆ ∪ ( 𝑥 ∩ 𝒫 𝑦 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctg	⊢ topGen
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5	1	cv	⊢ 𝑥
6	4	cpw	⊢ 𝒫 𝑦
7	5 6	cin	⊢ ( 𝑥 ∩ 𝒫 𝑦 )
8	7	cuni	⊢ ∪ ( 𝑥 ∩ 𝒫 𝑦 )
9	4 8	wss	⊢ 𝑦 ⊆ ∪ ( 𝑥 ∩ 𝒫 𝑦 )
10	9 3	cab	⊢ { 𝑦 ∣ 𝑦 ⊆ ∪ ( 𝑥 ∩ 𝒫 𝑦 ) }
11	1 2 10	cmpt	⊢ ( 𝑥 ∈ V ↦ { 𝑦 ∣ 𝑦 ⊆ ∪ ( 𝑥 ∩ 𝒫 𝑦 ) } )
12	0 11	wceq	⊢ topGen = ( 𝑥 ∈ V ↦ { 𝑦 ∣ 𝑦 ⊆ ∪ ( 𝑥 ∩ 𝒫 𝑦 ) } )

Metamath Proof Explorer

Definition df-topgen

Detailed syntax breakdown