chincl

Description: Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chincl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \cap B \in C_{ℋ}$

Step	Hyp	Ref	Expression
1		ineq1	$⊢ A = if (A \in C_{ℋ}, A, ℋ) \to A \cap B = if (A \in C_{ℋ}, A, ℋ) \cap B$
2	1	eleq1d	$⊢ A = if (A \in C_{ℋ}, A, ℋ) \to (A \cap B \in C_{ℋ} \leftrightarrow if (A \in C_{ℋ}, A, ℋ) \cap B \in C_{ℋ})$
3		ineq2	$⊢ B = if (B \in C_{ℋ}, B, ℋ) \to if (A \in C_{ℋ}, A, ℋ) \cap B = if (A \in C_{ℋ}, A, ℋ) \cap if (B \in C_{ℋ}, B, ℋ)$
4	3	eleq1d	$⊢ B = if (B \in C_{ℋ}, B, ℋ) \to (if (A \in C_{ℋ}, A, ℋ) \cap B \in C_{ℋ} \leftrightarrow if (A \in C_{ℋ}, A, ℋ) \cap if (B \in C_{ℋ}, B, ℋ) \in C_{ℋ})$
5		ifchhv	$⊢ if (A \in C_{ℋ}, A, ℋ) \in C_{ℋ}$
6		ifchhv	$⊢ if (B \in C_{ℋ}, B, ℋ) \in C_{ℋ}$
7	5 6	chincli	$⊢ if (A \in C_{ℋ}, A, ℋ) \cap if (B \in C_{ℋ}, B, ℋ) \in C_{ℋ}$
8	2 4 7	dedth2h	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to A \cap B \in C_{ℋ}$

Metamath Proof Explorer