chcv2

Description: The Hilbert lattice has the covering property. (Contributed by NM, 11-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chcv2	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \subset A \lor_{ℋ} B \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$

Step	Hyp	Ref	Expression
1		atelch	$⊢ B \in HAtoms \to B \in C_{ℋ}$
2		chnle	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\neg B \subseteq A \leftrightarrow A \subset A \lor_{ℋ} B)$
3	1 2	sylan2	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A \subset A \lor_{ℋ} B)$
4		chcv1	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (\neg B \subseteq A \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$
5	3 4	bitr3d	$⊢ (A \in C_{ℋ} \land B \in HAtoms) \to (A \subset A \lor_{ℋ} B \leftrightarrow A ⋖_{ℋ} (A \lor_{ℋ} B))$

Metamath Proof Explorer