Theorem oplecon3b 29683

Description: Contraposition law for orthoposets. (chsscon3 22955 analog.) (Contributed by NM, 4-Nov-2011.)

Hypotheses

Ref	Expression
opcon3.b	|- B = ( Base ` K )
opcon3.l	|- .<_ = ( le ` K )
opcon3.o	|- ._|_ = ( oc ` K )

Assertion

Ref	Expression
oplecon3b	|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )

Proof of Theorem oplecon3b

Step	Hyp	Ref	Expression
1		opcon3.b	. . 3 |- B = ( Base ` K )
2		opcon3.l	. . 3 |- .<_ = ( le ` K )
3		opcon3.o	. . 3 |- ._|_ = ( oc ` K )
4	1, 2, 3	oplecon3 29682	. 2 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
5		simp1 957	. . . 4 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> K e. OP )
6	1, 3	opoccl 29677	. . . . 5 |- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
7	6	3adant2 976	. . . 4 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` Y ) e. B )
8	1, 3	opoccl 29677	. . . . 5 |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` X ) e. B )
9	8	3adant3 977	. . . 4 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` X ) e. B )
10	1, 2, 3	oplecon3 29682	. . . 4 |- ( ( K e. OP /\ ( ._|_ ` Y ) e. B /\ ( ._|_ ` X ) e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) ) )
11	5, 7, 9, 10	syl3anc 1184	. . 3 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) ) )
12	1, 3	opococ 29678	. . . . 5 |- ( ( K e. OP /\ X e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
13	12	3adant3 977	. . . 4 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
14	1, 3	opococ 29678	. . . . 5 |- ( ( K e. OP /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
15	14	3adant2 976	. . . 4 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ._|_ ` ( ._|_ ` Y ) ) = Y )
16	13, 15	breq12d 4185	. . 3 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` ( ._|_ ` X ) ) .<_ ( ._|_ ` ( ._|_ ` Y ) ) <-> X .<_ Y ) )
17	11, 16	sylibd 206	. 2 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ._|_ ` Y ) .<_ ( ._|_ ` X ) -> X .<_ Y ) )
18	4, 17	impbid 184	1 |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ w3a 936   = wceq 1649   e. wcel 1721   class class class wbr 4172   ` cfv 5413   Basecbs 13424   lecple 13491   occoc 13492   OPcops 29655

This theorem is referenced by:  oplecon1b  29684  opltcon3b  29687  oldmm1  29700  omllaw4  29729  cvrcmp2  29767  glbconN  29859  lhpmod2i2  30520  lhpmod6i1  30521  lhprelat3N  30522  dochss  31848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-oposet 29659