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

Metamath Proof Explorer

Theorem chsscon3i

Description: Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 
|- A e. CH
chjcl.2 
|- B e. CH
Assertion chsscon3i 
|- ( A C_ B <-> ( _|_ ` B ) C_ ( _|_ ` A ) )

Proof

Step Hyp Ref Expression
1 ch0le.1 
 |-  A e. CH
2 chjcl.2 
 |-  B e. CH
3 1 chssii 
 |-  A C_ ~H
4 2 chssii 
 |-  B C_ ~H
5 occon 
 |-  ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) ) )
6 3 4 5 mp2an 
 |-  ( A C_ B -> ( _|_ ` B ) C_ ( _|_ ` A ) )
7 2 choccli 
 |-  ( _|_ ` B ) e. CH
8 7 chssii 
 |-  ( _|_ ` B ) C_ ~H
9 1 choccli 
 |-  ( _|_ ` A ) e. CH
10 9 chssii 
 |-  ( _|_ ` A ) C_ ~H
11 occon 
 |-  ( ( ( _|_ ` B ) C_ ~H /\ ( _|_ ` A ) C_ ~H ) -> ( ( _|_ ` B ) C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) ) )
12 8 10 11 mp2an 
 |-  ( ( _|_ ` B ) C_ ( _|_ ` A ) -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) )
13 1 pjococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
14 2 pjococi 
 |-  ( _|_ ` ( _|_ ` B ) ) = B
15 12 13 14 3sstr3g 
 |-  ( ( _|_ ` B ) C_ ( _|_ ` A ) -> A C_ B )
16 6 15 impbii 
 |-  ( A C_ B <-> ( _|_ ` B ) C_ ( _|_ ` A ) )