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 ralrimivw 
 |-  ( A C_ B -> A. x e. ~H ( A. y e. B ( x .ih y ) = 0 -> A. y e. A ( x .ih y ) = 0 ) )
3 ss2rab 
 |-  ( { x e. ~H | A. y e. B ( x .ih y ) = 0 } C_ { x e. ~H | A. y e. A ( x .ih y ) = 0 } <-> A. x e. ~H ( A. y e. B ( x .ih y ) = 0 -> A. y e. A ( x .ih y ) = 0 ) )
4 2 3 sylibr 
 |-  ( 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 4 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 } )
6 ocval 
 |-  ( B C_ ~H -> ( _|_ ` B ) = { x e. ~H | A. y e. B ( x .ih y ) = 0 } )
7 6 ad2antlr 
 |-  ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` B ) = { x e. ~H | A. y e. B ( x .ih y ) = 0 } )
8 ocval 
 |-  ( A C_ ~H -> ( _|_ ` A ) = { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
9 8 ad2antrr 
 |-  ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` A ) = { x e. ~H | A. y e. A ( x .ih y ) = 0 } )
10 5 7 9 3sstr4d 
 |-  ( ( ( A C_ ~H /\ B C_ ~H ) /\ A C_ B ) -> ( _|_ ` B ) C_ ( _|_ ` A ) )
11 10 ex 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) ) )