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 ∧ 𝐶 ∈ 𝐵 ) ∧ ( 𝐷 ∈ 𝐵 ∧ 𝐴 ∈ ( 𝐶 ∩ 𝐷 ) ) ) → ∃ 𝑥 ∈ 𝐵 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ ( 𝐶 ∩ 𝐷 ) ) )