# Metamath Proof Explorer

## Theorem isopos

Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011) (Revised by NM, 14-Sep-2018)

Ref Expression
Hypotheses isopos.b
`|- B = ( Base ` K )`
isopos.e
`|- U = ( lub ` K )`
isopos.g
`|- G = ( glb ` K )`
isopos.l
`|- .<_ = ( le ` K )`
isopos.o
`|- ._|_ = ( oc ` K )`
isopos.j
`|- .\/ = ( join ` K )`
isopos.m
`|- ./\ = ( meet ` K )`
isopos.f
`|- .0. = ( 0. ` K )`
isopos.u
`|- .1. = ( 1. ` K )`
Assertion isopos
`|- ( K e. OP <-> ( ( K e. Poset /\ B e. dom U /\ B e. dom G ) /\ A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )`

### Proof

Step Hyp Ref Expression
1 isopos.b
` |-  B = ( Base ` K )`
2 isopos.e
` |-  U = ( lub ` K )`
3 isopos.g
` |-  G = ( glb ` K )`
4 isopos.l
` |-  .<_ = ( le ` K )`
5 isopos.o
` |-  ._|_ = ( oc ` K )`
6 isopos.j
` |-  .\/ = ( join ` K )`
7 isopos.m
` |-  ./\ = ( meet ` K )`
8 isopos.f
` |-  .0. = ( 0. ` K )`
9 isopos.u
` |-  .1. = ( 1. ` K )`
10 fveq2
` |-  ( p = K -> ( Base ` p ) = ( Base ` K ) )`
11 10 1 eqtr4di
` |-  ( p = K -> ( Base ` p ) = B )`
12 fveq2
` |-  ( p = K -> ( lub ` p ) = ( lub ` K ) )`
13 12 2 eqtr4di
` |-  ( p = K -> ( lub ` p ) = U )`
14 13 dmeqd
` |-  ( p = K -> dom ( lub ` p ) = dom U )`
15 11 14 eleq12d
` |-  ( p = K -> ( ( Base ` p ) e. dom ( lub ` p ) <-> B e. dom U ) )`
16 fveq2
` |-  ( p = K -> ( glb ` p ) = ( glb ` K ) )`
17 16 3 eqtr4di
` |-  ( p = K -> ( glb ` p ) = G )`
18 17 dmeqd
` |-  ( p = K -> dom ( glb ` p ) = dom G )`
19 11 18 eleq12d
` |-  ( p = K -> ( ( Base ` p ) e. dom ( glb ` p ) <-> B e. dom G ) )`
20 15 19 anbi12d
` |-  ( p = K -> ( ( ( Base ` p ) e. dom ( lub ` p ) /\ ( Base ` p ) e. dom ( glb ` p ) ) <-> ( B e. dom U /\ B e. dom G ) ) )`
21 fveq2
` |-  ( p = K -> ( oc ` p ) = ( oc ` K ) )`
22 21 5 eqtr4di
` |-  ( p = K -> ( oc ` p ) = ._|_ )`
23 22 eqeq2d
` |-  ( p = K -> ( n = ( oc ` p ) <-> n = ._|_ ) )`
24 11 eleq2d
` |-  ( p = K -> ( ( n ` x ) e. ( Base ` p ) <-> ( n ` x ) e. B ) )`
25 fveq2
` |-  ( p = K -> ( le ` p ) = ( le ` K ) )`
26 25 4 eqtr4di
` |-  ( p = K -> ( le ` p ) = .<_ )`
27 26 breqd
` |-  ( p = K -> ( x ( le ` p ) y <-> x .<_ y ) )`
28 26 breqd
` |-  ( p = K -> ( ( n ` y ) ( le ` p ) ( n ` x ) <-> ( n ` y ) .<_ ( n ` x ) ) )`
29 27 28 imbi12d
` |-  ( p = K -> ( ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) <-> ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) )`
30 24 29 3anbi13d
` |-  ( p = K -> ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) <-> ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) ) )`
31 fveq2
` |-  ( p = K -> ( join ` p ) = ( join ` K ) )`
32 31 6 eqtr4di
` |-  ( p = K -> ( join ` p ) = .\/ )`
33 32 oveqd
` |-  ( p = K -> ( x ( join ` p ) ( n ` x ) ) = ( x .\/ ( n ` x ) ) )`
34 fveq2
` |-  ( p = K -> ( 1. ` p ) = ( 1. ` K ) )`
35 34 9 eqtr4di
` |-  ( p = K -> ( 1. ` p ) = .1. )`
36 33 35 eqeq12d
` |-  ( p = K -> ( ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) <-> ( x .\/ ( n ` x ) ) = .1. ) )`
37 fveq2
` |-  ( p = K -> ( meet ` p ) = ( meet ` K ) )`
38 37 7 eqtr4di
` |-  ( p = K -> ( meet ` p ) = ./\ )`
39 38 oveqd
` |-  ( p = K -> ( x ( meet ` p ) ( n ` x ) ) = ( x ./\ ( n ` x ) ) )`
40 fveq2
` |-  ( p = K -> ( 0. ` p ) = ( 0. ` K ) )`
41 40 8 eqtr4di
` |-  ( p = K -> ( 0. ` p ) = .0. )`
42 39 41 eqeq12d
` |-  ( p = K -> ( ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) <-> ( x ./\ ( n ` x ) ) = .0. ) )`
43 30 36 42 3anbi123d
` |-  ( p = K -> ( ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) <-> ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) )`
44 11 43 raleqbidv
` |-  ( p = K -> ( A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) <-> A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) )`
45 11 44 raleqbidv
` |-  ( p = K -> ( A. x e. ( Base ` p ) A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) <-> A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) )`
46 23 45 anbi12d
` |-  ( p = K -> ( ( n = ( oc ` p ) /\ A. x e. ( Base ` p ) A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) ) <-> ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) )`
47 46 exbidv
` |-  ( p = K -> ( E. n ( n = ( oc ` p ) /\ A. x e. ( Base ` p ) A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) ) <-> E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) )`
48 20 47 anbi12d
` |-  ( p = K -> ( ( ( ( Base ` p ) e. dom ( lub ` p ) /\ ( Base ` p ) e. dom ( glb ` p ) ) /\ E. n ( n = ( oc ` p ) /\ A. x e. ( Base ` p ) A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) ) ) <-> ( ( B e. dom U /\ B e. dom G ) /\ E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) ) )`
49 df-oposet
` |-  OP = { p e. Poset | ( ( ( Base ` p ) e. dom ( lub ` p ) /\ ( Base ` p ) e. dom ( glb ` p ) ) /\ E. n ( n = ( oc ` p ) /\ A. x e. ( Base ` p ) A. y e. ( Base ` p ) ( ( ( n ` x ) e. ( Base ` p ) /\ ( n ` ( n ` x ) ) = x /\ ( x ( le ` p ) y -> ( n ` y ) ( le ` p ) ( n ` x ) ) ) /\ ( x ( join ` p ) ( n ` x ) ) = ( 1. ` p ) /\ ( x ( meet ` p ) ( n ` x ) ) = ( 0. ` p ) ) ) ) }`
50 48 49 elrab2
` |-  ( K e. OP <-> ( K e. Poset /\ ( ( B e. dom U /\ B e. dom G ) /\ E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) ) )`
51 anass
` |-  ( ( ( K e. Poset /\ ( B e. dom U /\ B e. dom G ) ) /\ E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) <-> ( K e. Poset /\ ( ( B e. dom U /\ B e. dom G ) /\ E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) ) )`
52 3anass
` |-  ( ( K e. Poset /\ B e. dom U /\ B e. dom G ) <-> ( K e. Poset /\ ( B e. dom U /\ B e. dom G ) ) )`
53 52 bicomi
` |-  ( ( K e. Poset /\ ( B e. dom U /\ B e. dom G ) ) <-> ( K e. Poset /\ B e. dom U /\ B e. dom G ) )`
54 5 fvexi
` |-  ._|_ e. _V`
55 fveq1
` |-  ( n = ._|_ -> ( n ` x ) = ( ._|_ ` x ) )`
56 55 eleq1d
` |-  ( n = ._|_ -> ( ( n ` x ) e. B <-> ( ._|_ ` x ) e. B ) )`
57 id
` |-  ( n = ._|_ -> n = ._|_ )`
58 57 55 fveq12d
` |-  ( n = ._|_ -> ( n ` ( n ` x ) ) = ( ._|_ ` ( ._|_ ` x ) ) )`
59 58 eqeq1d
` |-  ( n = ._|_ -> ( ( n ` ( n ` x ) ) = x <-> ( ._|_ ` ( ._|_ ` x ) ) = x ) )`
60 fveq1
` |-  ( n = ._|_ -> ( n ` y ) = ( ._|_ ` y ) )`
61 60 55 breq12d
` |-  ( n = ._|_ -> ( ( n ` y ) .<_ ( n ` x ) <-> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) )`
62 61 imbi2d
` |-  ( n = ._|_ -> ( ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) <-> ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) )`
63 56 59 62 3anbi123d
` |-  ( n = ._|_ -> ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) <-> ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) ) )`
64 55 oveq2d
` |-  ( n = ._|_ -> ( x .\/ ( n ` x ) ) = ( x .\/ ( ._|_ ` x ) ) )`
65 64 eqeq1d
` |-  ( n = ._|_ -> ( ( x .\/ ( n ` x ) ) = .1. <-> ( x .\/ ( ._|_ ` x ) ) = .1. ) )`
66 55 oveq2d
` |-  ( n = ._|_ -> ( x ./\ ( n ` x ) ) = ( x ./\ ( ._|_ ` x ) ) )`
67 66 eqeq1d
` |-  ( n = ._|_ -> ( ( x ./\ ( n ` x ) ) = .0. <-> ( x ./\ ( ._|_ ` x ) ) = .0. ) )`
68 63 65 67 3anbi123d
` |-  ( n = ._|_ -> ( ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) <-> ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )`
69 68 2ralbidv
` |-  ( n = ._|_ -> ( A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) <-> A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )`
70 54 69 ceqsexv
` |-  ( E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) <-> A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) )`
71 53 70 anbi12i
` |-  ( ( ( K e. Poset /\ ( B e. dom U /\ B e. dom G ) ) /\ E. n ( n = ._|_ /\ A. x e. B A. y e. B ( ( ( n ` x ) e. B /\ ( n ` ( n ` x ) ) = x /\ ( x .<_ y -> ( n ` y ) .<_ ( n ` x ) ) ) /\ ( x .\/ ( n ` x ) ) = .1. /\ ( x ./\ ( n ` x ) ) = .0. ) ) ) <-> ( ( K e. Poset /\ B e. dom U /\ B e. dom G ) /\ A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )`
72 50 51 71 3bitr2i
` |-  ( K e. OP <-> ( ( K e. Poset /\ B e. dom U /\ B e. dom G ) /\ A. x e. B A. y e. B ( ( ( ._|_ ` x ) e. B /\ ( ._|_ ` ( ._|_ ` x ) ) = x /\ ( x .<_ y -> ( ._|_ ` y ) .<_ ( ._|_ ` x ) ) ) /\ ( x .\/ ( ._|_ ` x ) ) = .1. /\ ( x ./\ ( ._|_ ` x ) ) = .0. ) ) )`