Metamath Proof Explorer

Theorem occon3

Description: Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ococss 
 |-  ( B C_ ~H -> B C_ ( _|_ ` ( _|_ ` B ) ) )
2 1 adantl 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> B C_ ( _|_ ` ( _|_ ` B ) ) )
3 ocss 
 |-  ( B C_ ~H -> ( _|_ ` B ) C_ ~H )
4 occon 
 |-  ( ( A C_ ~H /\ ( _|_ ` B ) C_ ~H ) -> ( A C_ ( _|_ ` B ) -> ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) ) )
5 3 4 sylan2 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) -> ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) ) )
6 sstr2 
 |-  ( B C_ ( _|_ ` ( _|_ ` B ) ) -> ( ( _|_ ` ( _|_ ` B ) ) C_ ( _|_ ` A ) -> B C_ ( _|_ ` A ) ) )
7 2 5 6 sylsyld 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) -> B C_ ( _|_ ` A ) ) )
8 ococss 
 |-  ( A C_ ~H -> A C_ ( _|_ ` ( _|_ ` A ) ) )
9 8 adantr 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> A C_ ( _|_ ` ( _|_ ` A ) ) )
10 id 
 |-  ( B C_ ~H -> B C_ ~H )
11 ocss 
 |-  ( A C_ ~H -> ( _|_ ` A ) C_ ~H )
12 occon 
 |-  ( ( B C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( B C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) ) )
13 10 11 12 syl2anr 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( B C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) ) )
14 sstr2 
 |-  ( A C_ ( _|_ ` ( _|_ ` A ) ) -> ( ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` B ) -> A C_ ( _|_ ` B ) ) )
15 9 13 14 sylsyld 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( B C_ ( _|_ ` A ) -> A C_ ( _|_ ` B ) ) )
16 7 15 impbid 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) )