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