This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )