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

Metamath Proof Explorer

Theorem chsscon2

Description: Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	chsscon2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$

Step	Hyp	Ref	Expression
1		chss	$⊢ A \in C_{ℋ} \to A \subseteq ℋ$
2		chss	$⊢ B \in C_{ℋ} \to B \subseteq ℋ$
3		occon3	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$
4	1 2 3	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$