Definition df-bases

Description: Define the class of topological bases. Equivalent to definition of basis in Munkres p. 78 (see isbasis2g ). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006)

	Ref	Expression
Assertion	df-bases	⊢ TopBases = { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctb	⊢ TopBases
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		vz	⊢ 𝑧
5	2	cv	⊢ 𝑦
6	4	cv	⊢ 𝑧
7	5 6	cin	⊢ ( 𝑦 ∩ 𝑧 )
8	7	cpw	⊢ 𝒫 ( 𝑦 ∩ 𝑧 )
9	3 8	cin	⊢ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
10	9	cuni	⊢ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
11	7 10	wss	⊢ ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
12	11 4 3	wral	⊢ ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
13	12 2 3	wral	⊢ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) )
14	13 1	cab	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) }
15	0 14	wceq	⊢ TopBases = { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) }