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

Metamath Proof Explorer

Theorem basis1

Description: Property of a basis. (Contributed by NM, 16-Jul-2006)

Ref Expression
Assertion basis1 ( ( 𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 isbasisg ⊢ ( 𝐵 ∈ TopBases → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
2 1 ibi ⊢ ( 𝐵 ∈ TopBases → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
3 ineq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∩ 𝑦 ) = ( 𝐶 ∩ 𝑦 ) )
4 3 pweqd ⊢ ( 𝑥 = 𝐶 → 𝒫 ( 𝑥 ∩ 𝑦 ) = 𝒫 ( 𝐶 ∩ 𝑦 ) )
5 4 ineq2d ⊢ ( 𝑥 = 𝐶 → ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) )
6 5 unieqd ⊢ ( 𝑥 = 𝐶 → ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) = ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) )
7 3 6 sseq12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝐶 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) ) )
8 ineq2 ⊢ ( 𝑦 = 𝐷 → ( 𝐶 ∩ 𝑦 ) = ( 𝐶 ∩ 𝐷 ) )
9 8 pweqd ⊢ ( 𝑦 = 𝐷 → 𝒫 ( 𝐶 ∩ 𝑦 ) = 𝒫 ( 𝐶 ∩ 𝐷 ) )
10 9 ineq2d ⊢ ( 𝑦 = 𝐷 → ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) = ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) )
11 10 unieqd ⊢ ( 𝑦 = 𝐷 → ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) = ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) )
12 8 11 sseq12d ⊢ ( 𝑦 = 𝐷 → ( ( 𝐶 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝑦 ) ) ↔ ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) ) )
13 7 12 rspc2v ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) ) )
14 2 13 syl5com ⊢ ( 𝐵 ∈ TopBases → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) ) )
15 14 3impib ⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) )