occon

Description: Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000) (New usage is discouraged.)

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

Step	Hyp	Ref	Expression
1		ssralv	$⊢ A \subseteq B \to (\forall y \in B x \cdot_{ih} y = 0 \to \forall y \in A x \cdot_{ih} y = 0)$
2	1	adantr	$⊢ (A \subseteq B \land x \in ℋ) \to (\forall y \in B x \cdot_{ih} y = 0 \to \forall y \in A x \cdot_{ih} y = 0)$
3	2	ss2rabdv	$⊢ A \subseteq B \to \{x \in ℋ \| \forall y \in B x \cdot_{ih} y = 0\} \subseteq \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\}$
4	3	adantl	$⊢ ((A \subseteq ℋ \land B \subseteq ℋ) \land A \subseteq B) \to \{x \in ℋ \| \forall y \in B x \cdot_{ih} y = 0\} \subseteq \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\}$
5		ocval	$⊢ B \subseteq ℋ \to ⊥ (B) = \{x \in ℋ \| \forall y \in B x \cdot_{ih} y = 0\}$
6	5	ad2antlr	$⊢ ((A \subseteq ℋ \land B \subseteq ℋ) \land A \subseteq B) \to ⊥ (B) = \{x \in ℋ \| \forall y \in B x \cdot_{ih} y = 0\}$
7		ocval	$⊢ A \subseteq ℋ \to ⊥ (A) = \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\}$
8	7	ad2antrr	$⊢ ((A \subseteq ℋ \land B \subseteq ℋ) \land A \subseteq B) \to ⊥ (A) = \{x \in ℋ \| \forall y \in A x \cdot_{ih} y = 0\}$
9	4 6 8	3sstr4d	$⊢ ((A \subseteq ℋ \land B \subseteq ℋ) \land A \subseteq B) \to ⊥ (B) \subseteq ⊥ (A)$
10	9	ex	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq B \to ⊥ (B) \subseteq ⊥ (A))$

Metamath Proof Explorer