Metamath Proof Explorer

Theorem oposlem

Description: Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011)

Ref Expression
Hypotheses oposlem.b 
|- B = ( Base ` K )
oposlem.l 
|- .<_ = ( le ` K )
oposlem.o 
|- ._|_ = ( oc ` K )
oposlem.j 
|- .\/ = ( join ` K )
oposlem.m 
|- ./\ = ( meet ` K )
oposlem.f 
|- .0. = ( 0. ` K )
oposlem.u 
|- .1. = ( 1. ` K )
Assertion oposlem 
|- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) )

Proof

Step Hyp Ref Expression
1 oposlem.b 
 |-  B = ( Base ` K )
2 oposlem.l 
 |-  .<_ = ( le ` K )
3 oposlem.o 
 |-  ._|_ = ( oc ` K )
4 oposlem.j 
 |-  .\/ = ( join ` K )
5 oposlem.m 
 |-  ./\ = ( meet ` K )
6 oposlem.f 
 |-  .0. = ( 0. ` K )
7 oposlem.u 
 |-  .1. = ( 1. ` K )
8 eqid 
 |-  ( lub ` K ) = ( lub ` K )
9 eqid 
 |-  ( glb ` K ) = ( glb ` K )
10 1 8 9 2 3 4 5 6 7 isopos 
 |-  ( K e. OP <-> ( ( K e. Poset /\ B e. dom ( lub ` K ) /\ B e. dom ( glb ` K ) ) /\ A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )
11 10 simprbi 
 |-  ( K e. OP -> A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) )
12 fveq2 
 |-  ( x = X -> ( ._|_ ` x ) = ( ._|_ ` X ) )
13 12 eleq1d 
 |-  ( x = X -> ( ( ._|_ ` x ) e. B <-> ( ._|_ ` X ) e. B ) )
14 2fveq3 
 |-  ( x = X -> ( ._|_ ` ( ._|_ ` x ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
15 id 
 |-  ( x = X -> x = X )
16 14 15 eqeq12d 
 |-  ( x = X -> ( ( ._|_ ` ( ._|_ ` x ) ) = x <-> ( ._|_ ` ( ._|_ ` X ) ) = X ) )
17 breq1 
 |-  ( x = X -> ( x .<_ y <-> X .<_ y ) )
18 12 breq2d 
 |-  ( x = X -> ( ( ._|_ ` y ) .<_ ( ._|_ ` x ) <-> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) )
19 17 18 imbi12d 
 |-  ( x = X -> ( ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) <-> ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) ) )
20 13 16 19 3anbi123d 
 |-  ( x = X -> ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) <-> ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) ) ) )
21 15 12 oveq12d 
 |-  ( x = X -> ( x .\/ ( ._|_ ` x ) ) = ( X .\/ ( ._|_ ` X ) ) )
22 21 eqeq1d 
 |-  ( x = X -> ( ( x .\/ ( ._|_ ` x ) ) = .1. <-> ( X .\/ ( ._|_ ` X ) ) = .1. ) )
23 15 12 oveq12d 
 |-  ( x = X -> ( x ./\ ( ._|_ ` x ) ) = ( X ./\ ( ._|_ ` X ) ) )
24 23 eqeq1d 
 |-  ( x = X -> ( ( x ./\ ( ._|_ ` x ) ) = .0. <-> ( X ./\ ( ._|_ ` X ) ) = .0. ) )
25 20 22 24 3anbi123d 
 |-  ( x = X -> ( ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) <-> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) ) )
26 breq2 
 |-  ( y = Y -> ( X .<_ y <-> X .<_ Y ) )
27 fveq2 
 |-  ( y = Y -> ( ._|_ ` y ) = ( ._|_ ` Y ) )
28 27 breq1d 
 |-  ( y = Y -> ( ( ._|_ ` y ) .<_ ( ._|_ ` X ) <-> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) )
29 26 28 imbi12d 
 |-  ( y = Y -> ( ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) <-> ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) )
30 29 3anbi3d 
 |-  ( y = Y -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) ) <-> ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) ) )
31 30 3anbi1d 
 |-  ( y = Y -> ( ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) <-> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) ) )
32 25 31 rspc2v 
 |-  ( ( X e. B /\ Y e. B ) -> ( A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) ) )
33 11 32 mpan9 
 |-  ( ( K e. OP /\ ( X e. B /\ Y e. B ) ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) )
34 33 3impb 
 |-  ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( ( ( ._|_ ` X ) e. B /\ ( ._|_ ` ( ._|_ ` X ) ) = X /\ ( X .<_ Y -> ( ._|_ ` Y ) .<_ ( ._|_ ` X ) ) ) /\ ( X .\/ ( ._|_ ` X ) ) = .1. /\ ( X ./\ ( ._|_ ` X ) ) = .0. ) )