chsscon3i

Description: Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ch0le.1	$⊢ A \in C_{ℋ}$
	chjcl.2	$⊢ B \in C_{ℋ}$
Assertion	chsscon3i	$⊢ A \subseteq B \leftrightarrow ⊥ (B) \subseteq ⊥ (A)$

Step	Hyp	Ref	Expression
1		ch0le.1	$⊢ A \in C_{ℋ}$
2		chjcl.2	$⊢ B \in C_{ℋ}$
3	1	chssii	$⊢ A \subseteq ℋ$
4	2	chssii	$⊢ B \subseteq ℋ$
5		occon	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq B \to ⊥ (B) \subseteq ⊥ (A))$
6	3 4 5	mp2an	$⊢ A \subseteq B \to ⊥ (B) \subseteq ⊥ (A)$
7	2	choccli	$⊢ ⊥ (B) \in C_{ℋ}$
8	7	chssii	$⊢ ⊥ (B) \subseteq ℋ$
9	1	choccli	$⊢ ⊥ (A) \in C_{ℋ}$
10	9	chssii	$⊢ ⊥ (A) \subseteq ℋ$
11		occon	$⊢ (⊥ (B) \subseteq ℋ \land ⊥ (A) \subseteq ℋ) \to (⊥ (B) \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (B)))$
12	8 10 11	mp2an	$⊢ ⊥ (B) \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (B))$
13	1	pjococi	$⊢ ⊥ (⊥ (A)) = A$
14	2	pjococi	$⊢ ⊥ (⊥ (B)) = B$
15	12 13 14	3sstr3g	$⊢ ⊥ (B) \subseteq ⊥ (A) \to A \subseteq B$
16	6 15	impbii	$⊢ A \subseteq B \leftrightarrow ⊥ (B) \subseteq ⊥ (A)$

Metamath Proof Explorer