occon3

Description: Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014) (New usage is discouraged.)

		Ref	Expression
	Assertion	occon3	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$

Step	Hyp	Ref	Expression
1		ococss	$⊢ B \subseteq ℋ \to B \subseteq ⊥ (⊥ (B))$
2	1	adantl	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to B \subseteq ⊥ (⊥ (B))$
3		ocss	$⊢ B \subseteq ℋ \to ⊥ (B) \subseteq ℋ$
4		occon	$⊢ (A \subseteq ℋ \land ⊥ (B) \subseteq ℋ) \to (A \subseteq ⊥ (B) \to ⊥ (⊥ (B)) \subseteq ⊥ (A))$
5	3 4	sylan2	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \to ⊥ (⊥ (B)) \subseteq ⊥ (A))$
6		sstr2	$⊢ B \subseteq ⊥ (⊥ (B)) \to (⊥ (⊥ (B)) \subseteq ⊥ (A) \to B \subseteq ⊥ (A))$
7	2 5 6	sylsyld	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \to B \subseteq ⊥ (A))$
8		ococss	$⊢ A \subseteq ℋ \to A \subseteq ⊥ (⊥ (A))$
9	8	adantr	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to A \subseteq ⊥ (⊥ (A))$
10		id	$⊢ B \subseteq ℋ \to B \subseteq ℋ$
11		ocss	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
12		occon	$⊢ (B \subseteq ℋ \land ⊥ (A) \subseteq ℋ) \to (B \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (B))$
13	10 11 12	syl2anr	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (B \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (B))$
14		sstr2	$⊢ A \subseteq ⊥ (⊥ (A)) \to (⊥ (⊥ (A)) \subseteq ⊥ (B) \to A \subseteq ⊥ (B))$
15	9 13 14	sylsyld	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (B \subseteq ⊥ (A) \to A \subseteq ⊥ (B))$
16	7 15	impbid	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$

Metamath Proof Explorer