Metamath Proof Explorer

Theorem occon2

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

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

Proof

Step Hyp Ref Expression
1 ocss 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
2 ocss 
 |-  ( B C_ ~H -> ( _|_ ` B ) C_ ~H )
3 1 2 anim12ci 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( ( _|_ ` B ) C_ ~H /\ ( _|_ ` A ) C_ ~H ) )
4 occon 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) ) )
5 occon 
 |-  ( ( ( _|_ ` B ) C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( ( _|_ ` B ) C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) ) )
6 3 4 5 sylsyld 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) ) )