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