Theorem occon

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

	Ref	Expression
Assertion	occon	|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssralv	|- ( A C_ B -> ( A. y e. B ( x .ih y ) = 0 -> A. y e. A ( x .ih y ) = 0 ) )
2	1	adantr	|- ( ( A C_ B /\ x e. ~H ) -> ( A. y e. B ( x .ih y ) = 0 -> A. y e. A ( x .ih y ) = 0 ) )
3	2	ss2rabdv	|- ( A C_ B -> { x e. ~H | A. y e. B ( x .ih y ) = 0 } C_ { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
4	3	adantl	|- ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> { x e. ~H | A. y e. B ( x .ih y ) = 0 } C_ { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
5		ocval	|- ( B C_ ~H -> ( _|_ ` B ) = { x e. ~H | A. y e. B ( x .ih y ) = 0 } )
6	5	ad2antlr	|- ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` B ) = { x e. ~H | A. y e. B ( x .ih y ) = 0 } )
7		ocval	|- ( A C_ ~H -> ( _|_ ` A ) = { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
8	7	ad2antrr	|- ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` A ) = { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
9	4 6 8	3sstr4d	|- ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` B ) C_ ( _|_ ` A ) )
10	9	ex	|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) ) )