occon2

Description: Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		ocss	$⊢ A \subseteq ℋ \to ⊥ (A) \subseteq ℋ$
2		ocss	$⊢ B \subseteq ℋ \to ⊥ (B) \subseteq ℋ$
3	1 2	anim12ci	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (⊥ (B) \subseteq ℋ \land ⊥ (A) \subseteq ℋ)$
4		occon	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq B \to ⊥ (B) \subseteq ⊥ (A))$
5		occon	$⊢ (⊥ (B) \subseteq ℋ \land ⊥ (A) \subseteq ℋ) \to (⊥ (B) \subseteq ⊥ (A) \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (B)))$
6	3 4 5	sylsyld	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq B \to ⊥ (⊥ (A)) \subseteq ⊥ (⊥ (B)))$

Metamath Proof Explorer