chpsscon2

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

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

Step	Hyp	Ref	Expression
1		choccl	$⊢ B \in C_{ℋ} \to ⊥ (B) \in C_{ℋ}$
2		chpsscon3	$⊢ (A \in C_{ℋ} \land ⊥ (B) \in C_{ℋ}) \to (A \subset ⊥ (B) \leftrightarrow ⊥ (⊥ (B)) \subset ⊥ (A))$
3	1 2	sylan2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subset ⊥ (B) \leftrightarrow ⊥ (⊥ (B)) \subset ⊥ (A))$
4		ococ	$⊢ B \in C_{ℋ} \to ⊥ (⊥ (B)) = B$
5	4	adantl	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (B)) = B$
6	5	psseq1d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (⊥ (B)) \subset ⊥ (A) \leftrightarrow B \subset ⊥ (A))$
7	3 6	bitrd	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subset ⊥ (B) \leftrightarrow B \subset ⊥ (A))$

Metamath Proof Explorer