This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lecmi

Description: Comparable Hilbert lattice elements commute. Theorem 2.3(iii) of Beran p. 40. (Contributed by NM, 16-Jan-2005) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjoml2.1	$⊢ A \in C_{ℋ}$
	pjoml2.2	$⊢ B \in C_{ℋ}$
Assertion	lecmi	$⊢ A \subseteq B \to A 𝐶_{ℋ} B$

Proof

Step	Hyp	Ref	Expression
1		pjoml2.1	$⊢ A \in C_{ℋ}$
2		pjoml2.2	$⊢ B \in C_{ℋ}$
3		ssinss1	$⊢ A \subseteq B \to A \cap (⊥ (A) \lor_{ℋ} B) \subseteq B$
4	1 2	cmbr4i	$⊢ A 𝐶_{ℋ} B \leftrightarrow A \cap (⊥ (A) \lor_{ℋ} B) \subseteq B$
5	3 4	sylibr	$⊢ A \subseteq B \to A 𝐶_{ℋ} B$