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