Definition df-bases 12641

Description: Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 12643). 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 12640	. 2 class TopBases
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1342	. . . . . . 7 class 𝑦
4		vz	. . . . . . . 8 setvar 𝑧
5	4	cv 1342	. . . . . . 7 class 𝑧
6	3, 5	cin 3114	. . . . . 6 class (𝑦 ∩ 𝑧)
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1342	. . . . . . . 8 class 𝑥
9	6	cpw 3558	. . . . . . . 8 class 𝒫 (𝑦 ∩ 𝑧)
10	8, 9	cin 3114	. . . . . . 7 class (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
11	10	cuni 3788	. . . . . 6 class ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
12	6, 11	wss 3115	. . . . 5 wff (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
13	12, 4, 8	wral 2443	. . . 4 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
14	13, 2, 8	wral 2443	. . 3 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))
15	14, 7	cab 2151	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}
16	1, 15	wceq 1343	1 wff TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))}

This definition is referenced by:  isbasisg  12642