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

Metamath Proof Explorer

Theorem basis2

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

Ref Expression
Assertion basis2 ( ( ( 𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐷 ∈ 𝐵 ∧ 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢ ( 𝐵 ∈ TopBases → ( 𝐵 ∈ TopBases ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ) )
2 1 ibi ⊢ ( 𝐵 ∈ TopBases → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) )
3 ineq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∩ 𝑧 ) = ( 𝐶 ∩ 𝑧 ) )
4 sseq2 ⊢ ( ( 𝑦 ∩ 𝑧 ) = ( 𝐶 ∩ 𝑧 ) → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ↔ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) )
5 4 anbi2d ⊢ ( ( 𝑦 ∩ 𝑧 ) = ( 𝐶 ∩ 𝑧 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ) )
6 5 rexbidv ⊢ ( ( 𝑦 ∩ 𝑧 ) = ( 𝐶 ∩ 𝑧 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ) )
7 6 raleqbi1dv ⊢ ( ( 𝑦 ∩ 𝑧 ) = ( 𝐶 ∩ 𝑧 ) → ( ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ↔ ∀ 𝑤 ∈ ( 𝐶 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ) )
8 3 7 syl ⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ↔ ∀ 𝑤 ∈ ( 𝐶 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ) )
9 ineq2 ⊢ ( 𝑧 = 𝐷 → ( 𝐶 ∩ 𝑧 ) = ( 𝐶 ∩ 𝐷 ) )
10 sseq2 ⊢ ( ( 𝐶 ∩ 𝑧 ) = ( 𝐶 ∩ 𝐷 ) → ( 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ↔ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) )
11 10 anbi2d ⊢ ( ( 𝐶 ∩ 𝑧 ) = ( 𝐶 ∩ 𝐷 ) → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
12 11 rexbidv ⊢ ( ( 𝐶 ∩ 𝑧 ) = ( 𝐶 ∩ 𝐷 ) → ( ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
13 12 raleqbi1dv ⊢ ( ( 𝐶 ∩ 𝑧 ) = ( 𝐶 ∩ 𝐷 ) → ( ∀ 𝑤 ∈ ( 𝐶 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ↔ ∀ 𝑤 ∈ ( 𝐶 ∩ 𝐷 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
14 9 13 syl ⊢ ( 𝑧 = 𝐷 → ( ∀ 𝑤 ∈ ( 𝐶 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝑧 ) ) ↔ ∀ 𝑤 ∈ ( 𝐶 ∩ 𝐷 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
15 8 14 rspc2v ⊢ ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) → ∀ 𝑤 ∈ ( 𝐶 ∩ 𝐷 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
16 eleq1 ⊢ ( 𝑤 = 𝐴 → ( 𝑤 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
17 16 anbi1d ⊢ ( 𝑤 = 𝐴 → ( ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ↔ ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
18 17 rexbidv ⊢ ( 𝑤 = 𝐴 → ( ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ↔ ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
19 18 rspccv ⊢ ( ∀ 𝑤 ∈ ( 𝐶 ∩ 𝐷 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) → ( 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) )
20 15 19 syl6com ⊢ ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ ( 𝑦 ∩ 𝑧 ) ∃ 𝑥 ∈ 𝐵 ( 𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) ) )
21 2 20 syl ⊢ ( 𝐵 ∈ TopBases → ( ( 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) ) )
22 21 expd ⊢ ( 𝐵 ∈ TopBases → ( 𝐶 ∈ 𝐵 → ( 𝐷 ∈ 𝐵 → ( 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) ) ) ) )
23 22 imp43 ⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐷 ∈ 𝐵 ∧ 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) )