Metamath Proof Explorer

Theorem basis2

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

Ref Expression
Assertion basis2 ⊢ B ∈ TopBases ∧ C ∈ B ∧ D ∈ B ∧ A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢ B ∈ TopBases → B ∈ TopBases ↔ ∀ y ∈ B ∀ z ∈ B ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z
2 1 ibi ⊢ B ∈ TopBases → ∀ y ∈ B ∀ z ∈ B ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z
3 ineq1 ⊢ y = C → y ∩ z = C ∩ z
4 sseq2 ⊢ y ∩ z = C ∩ z → x ⊆ y ∩ z ↔ x ⊆ C ∩ z
5 4 anbi2d ⊢ y ∩ z = C ∩ z → w ∈ x ∧ x ⊆ y ∩ z ↔ w ∈ x ∧ x ⊆ C ∩ z
6 5 rexbidv ⊢ y ∩ z = C ∩ z → ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z ↔ ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z
7 6 raleqbi1dv ⊢ y ∩ z = C ∩ z → ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z ↔ ∀ w ∈ C ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z
8 3 7 syl ⊢ y = C → ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z ↔ ∀ w ∈ C ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z
9 ineq2 ⊢ z = D → C ∩ z = C ∩ D
10 sseq2 ⊢ C ∩ z = C ∩ D → x ⊆ C ∩ z ↔ x ⊆ C ∩ D
11 10 anbi2d ⊢ C ∩ z = C ∩ D → w ∈ x ∧ x ⊆ C ∩ z ↔ w ∈ x ∧ x ⊆ C ∩ D
12 11 rexbidv ⊢ C ∩ z = C ∩ D → ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z ↔ ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D
13 12 raleqbi1dv ⊢ C ∩ z = C ∩ D → ∀ w ∈ C ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z ↔ ∀ w ∈ C ∩ D ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D
14 9 13 syl ⊢ z = D → ∀ w ∈ C ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ z ↔ ∀ w ∈ C ∩ D ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D
15 8 14 rspc2v ⊢ C ∈ B ∧ D ∈ B → ∀ y ∈ B ∀ z ∈ B ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z → ∀ w ∈ C ∩ D ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D
16 eleq1 ⊢ w = A → w ∈ x ↔ A ∈ x
17 16 anbi1d ⊢ w = A → w ∈ x ∧ x ⊆ C ∩ D ↔ A ∈ x ∧ x ⊆ C ∩ D
18 17 rexbidv ⊢ w = A → ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D ↔ ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D
19 18 rspccv ⊢ ∀ w ∈ C ∩ D ∃ x ∈ B w ∈ x ∧ x ⊆ C ∩ D → A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D
20 15 19 syl6com ⊢ ∀ y ∈ B ∀ z ∈ B ∀ w ∈ y ∩ z ∃ x ∈ B w ∈ x ∧ x ⊆ y ∩ z → C ∈ B ∧ D ∈ B → A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D
21 2 20 syl ⊢ B ∈ TopBases → C ∈ B ∧ D ∈ B → A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D
22 21 expd ⊢ B ∈ TopBases → C ∈ B → D ∈ B → A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D
23 22 imp43 ⊢ B ∈ TopBases ∧ C ∈ B ∧ D ∈ B ∧ A ∈ C ∩ D → ∃ x ∈ B A ∈ x ∧ x ⊆ C ∩ D