chpsscon1

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

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

Step	Hyp	Ref	Expression
1		choccl	$⊢ A \in C_{ℋ} \to ⊥ (A) \in C_{ℋ}$
2		chpsscon3	$⊢ (⊥ (A) \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (A) \subset B \leftrightarrow ⊥ (B) \subset ⊥ (⊥ (A)))$
3	1 2	sylan	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (⊥ (A) \subset B \leftrightarrow ⊥ (B) \subset ⊥ (⊥ (A)))$
4		ococ	$⊢ A \in C_{ℋ} \to ⊥ (⊥ (A)) = A$
5	4	adantr	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ⊥ (⊥ (A)) = A$
6	5	psseq2d	$⊢ (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