chpsscon3

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

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

Step	Hyp	Ref	Expression
1		chsscon3	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq B \leftrightarrow ⊥ (B) \subseteq ⊥ (A))$
2		chsscon3	$⊢ (B \in C_{ℋ} \land A \in C_{ℋ}) \to (B \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (B))$
3	2	ancoms	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (B \subseteq A \leftrightarrow ⊥ (A) \subseteq ⊥ (B))$
4	3	notbid	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (\neg B \subseteq A \leftrightarrow \neg ⊥ (A) \subseteq ⊥ (B))$
5	1 4	anbi12d	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to ((A \subseteq B \land \neg B \subseteq A) \leftrightarrow (⊥ (B) \subseteq ⊥ (A) \land \neg ⊥ (A) \subseteq ⊥ (B)))$
6		dfpss3	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg B \subseteq A)$
7		dfpss3	$⊢ ⊥ (B) \subset ⊥ (A) \leftrightarrow (⊥ (B) \subseteq ⊥ (A) \land \neg ⊥ (A) \subseteq ⊥ (B))$
8	5 6 7	3bitr4g	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subset B \leftrightarrow ⊥ (B) \subset ⊥ (A))$

Metamath Proof Explorer