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∈BA∈x∧x⊆C∩D

Proof

Step Hyp Ref Expression
1 isbasis2g ⊢B∈TopBases→B∈TopBases↔∀y∈B∀z∈B∀w∈y∩z∃x∈Bw∈x∧x⊆y∩z
2 1 ibi ⊢B∈TopBases→∀y∈B∀z∈B∀w∈y∩z∃x∈Bw∈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∈Bw∈x∧x⊆y∩z↔∃x∈Bw∈x∧x⊆C∩z
7 6 raleqbi1dv ⊢y∩z=C∩z→∀w∈y∩z∃x∈Bw∈x∧x⊆y∩z↔∀w∈C∩z∃x∈Bw∈x∧x⊆C∩z
8 3 7 syl ⊢y=C→∀w∈y∩z∃x∈Bw∈x∧x⊆y∩z↔∀w∈C∩z∃x∈Bw∈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∈Bw∈x∧x⊆C∩z↔∃x∈Bw∈x∧x⊆C∩D
13 12 raleqbi1dv ⊢C∩z=C∩D→∀w∈C∩z∃x∈Bw∈x∧x⊆C∩z↔∀w∈C∩D∃x∈Bw∈x∧x⊆C∩D
14 9 13 syl ⊢z=D→∀w∈C∩z∃x∈Bw∈x∧x⊆C∩z↔∀w∈C∩D∃x∈Bw∈x∧x⊆C∩D
15 8 14 rspc2v ⊢C∈B∧D∈B→∀y∈B∀z∈B∀w∈y∩z∃x∈Bw∈x∧x⊆y∩z→∀w∈C∩D∃x∈Bw∈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∈Bw∈x∧x⊆C∩D↔∃x∈BA∈x∧x⊆C∩D
19 18 rspccv ⊢∀w∈C∩D∃x∈Bw∈x∧x⊆C∩D→A∈C∩D→∃x∈BA∈x∧x⊆C∩D
20 15 19 syl6com ⊢∀y∈B∀z∈B∀w∈y∩z∃x∈Bw∈x∧x⊆y∩z→C∈B∧D∈B→A∈C∩D→∃x∈BA∈x∧x⊆C∩D
21 2 20 syl ⊢B∈TopBases→C∈B∧D∈B→A∈C∩D→∃x∈BA∈x∧x⊆C∩D
22 21 expd ⊢B∈TopBases→C∈B→D∈B→A∈C∩D→∃x∈BA∈x∧x⊆C∩D
23 22 imp43 ⊢B∈TopBases∧C∈B∧D∈B∧A∈C∩D→∃x∈BA∈x∧x⊆C∩D