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 ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 ∩ 𝐷 ) ⊆ ∪ ( 𝐵 ∩ 𝒫 ( 𝐶 ∩ 𝐷 ) ) )