Definition df-bases 15235

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

Assertion

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

Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-bases

Step	Hyp	Ref	Expression
1		ctb 15234	. 2 class TopBases
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1401	. . . . . . 7 class 𝑦
4		vz	. . . . . . . 8 setvar 𝑧
5	4	cv 1401	. . . . . . 7 class 𝑧
6	3, 5	cin 3219	. . . . . 6 class (𝑦 ∩ 𝑧)
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1401	. . . . . . . 8 class 𝑥
9	6	cpw 3688	. . . . . . . 8 class 𝒫 (𝑦 ∩ 𝑧)
10	8, 9	cin 3219	. . . . . . 7 class (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
11	10	cuni 3935	. . . . . 6 class ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
12	6, 11	wss 3220	. . . . 5 wff (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
13	12, 4, 8	wral 2528	. . . 4 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
14	13, 2, 8	wral 2528	. . 3 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
15	14, 7	cab 2224	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
16	1, 15	wceq 1402	1 wff TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}

This definition is used by:  isbasisg  15236