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