This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ( 𝑦 ∩ 𝑧 ) ⊆ ∪ ( 𝑥 ∩ 𝒫 ( 𝑦 ∩ 𝑧 ) ) }