Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isopos Structured version   Visualization version   Unicode version

Theorem isopos 32791
Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011.) (Revised by NM, 14-Sep-2018.)
Hypotheses
Ref Expression
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
Ref Expression
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.  ) ) )
Distinct variable groups:    x, y, B    x,  ._|_ , y    x, K, y
Allowed substitution hints:    U( x, y)    .1. ( x, y)    G( x, y)    .\/ ( x, y)    .<_ ( x, y)    ./\ ( x, y)    .0. ( x, y)

Proof of Theorem isopos
Dummy variables  n  p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5888 . . . . . . 7  |-  ( p  =  K  ->  ( Base `  p )  =  ( Base `  K
) )
2 isopos.b . . . . . . 7  |-  B  =  ( Base `  K
)
31, 2syl6eqr 2514 . . . . . 6  |-  ( p  =  K  ->  ( Base `  p )  =  B )
4 fveq2 5888 . . . . . . . 8  |-  ( p  =  K  ->  ( lub `  p )  =  ( lub `  K
) )
5 isopos.e . . . . . . . 8  |-  U  =  ( lub `  K
)
64, 5syl6eqr 2514 . . . . . . 7  |-  ( p  =  K  ->  ( lub `  p )  =  U )
76dmeqd 5056 . . . . . 6  |-  ( p  =  K  ->  dom  ( lub `  p )  =  dom  U )
83, 7eleq12d 2534 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( lub `  p
)  <->  B  e.  dom  U ) )
9 fveq2 5888 . . . . . . . 8  |-  ( p  =  K  ->  ( glb `  p )  =  ( glb `  K
) )
10 isopos.g . . . . . . . 8  |-  G  =  ( glb `  K
)
119, 10syl6eqr 2514 . . . . . . 7  |-  ( p  =  K  ->  ( glb `  p )  =  G )
1211dmeqd 5056 . . . . . 6  |-  ( p  =  K  ->  dom  ( glb `  p )  =  dom  G )
133, 12eleq12d 2534 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( glb `  p
)  <->  B  e.  dom  G ) )
148, 13anbi12d 722 . . . 4  |-  ( p  =  K  ->  (
( ( Base `  p
)  e.  dom  ( lub `  p )  /\  ( Base `  p )  e.  dom  ( glb `  p
) )  <->  ( B  e.  dom  U  /\  B  e.  dom  G ) ) )
15 fveq2 5888 . . . . . . . 8  |-  ( p  =  K  ->  ( oc `  p )  =  ( oc `  K
) )
16 isopos.o . . . . . . . 8  |-  ._|_  =  ( oc `  K )
1715, 16syl6eqr 2514 . . . . . . 7  |-  ( p  =  K  ->  ( oc `  p )  = 
._|_  )
1817eqeq2d 2472 . . . . . 6  |-  ( p  =  K  ->  (
n  =  ( oc
`  p )  <->  n  =  ._|_  ) )
193eleq2d 2525 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( n `  x
)  e.  ( Base `  p )  <->  ( n `  x )  e.  B
) )
20 fveq2 5888 . . . . . . . . . . . . 13  |-  ( p  =  K  ->  ( le `  p )  =  ( le `  K
) )
21 isopos.l . . . . . . . . . . . . 13  |-  .<_  =  ( le `  K )
2220, 21syl6eqr 2514 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( le `  p )  = 
.<_  )
2322breqd 4427 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
x ( le `  p ) y  <->  x  .<_  y ) )
2422breqd 4427 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
( n `  y
) ( le `  p ) ( n `
 x )  <->  ( n `  y )  .<_  ( n `
 x ) ) )
2523, 24imbi12d 326 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( x ( le
`  p ) y  ->  ( n `  y ) ( le
`  p ) ( n `  x ) )  <->  ( x  .<_  y  ->  ( n `  y )  .<_  ( n `
 x ) ) ) )
2619, 253anbi13d 1350 . . . . . . . . 9  |-  ( 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
) ) ) ) )
27 fveq2 5888 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( join `  p )  =  ( join `  K
) )
28 isopos.j . . . . . . . . . . . 12  |-  .\/  =  ( join `  K )
2927, 28syl6eqr 2514 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( join `  p )  = 
.\/  )
3029oveqd 6332 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( join `  p
) ( n `  x ) )  =  ( x  .\/  (
n `  x )
) )
31 fveq2 5888 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 1. `  p )  =  ( 1. `  K
) )
32 isopos.u . . . . . . . . . . 11  |-  .1.  =  ( 1. `  K )
3331, 32syl6eqr 2514 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 1. `  p )  =  .1.  )
3430, 33eqeq12d 2477 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( join `  p ) ( n `
 x ) )  =  ( 1. `  p )  <->  ( x  .\/  ( n `  x
) )  =  .1.  ) )
35 fveq2 5888 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( meet `  p )  =  ( meet `  K
) )
36 isopos.m . . . . . . . . . . . 12  |-  ./\  =  ( meet `  K )
3735, 36syl6eqr 2514 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( meet `  p )  = 
./\  )
3837oveqd 6332 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( meet `  p
) ( n `  x ) )  =  ( x  ./\  (
n `  x )
) )
39 fveq2 5888 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 0. `  p )  =  ( 0. `  K
) )
40 isopos.f . . . . . . . . . . 11  |-  .0.  =  ( 0. `  K )
4139, 40syl6eqr 2514 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 0. `  p )  =  .0.  )
4238, 41eqeq12d 2477 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( meet `  p ) ( n `
 x ) )  =  ( 0. `  p )  <->  ( x  ./\  ( n `  x
) )  =  .0.  ) )
4326, 34, 423anbi123d 1348 . . . . . . . 8  |-  ( 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.  ) ) )
443, 43raleqbidv 3013 . . . . . . 7  |-  ( 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.  ) ) )
453, 44raleqbidv 3013 . . . . . 6  |-  ( 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.  ) ) )
4618, 45anbi12d 722 . . . . 5  |-  ( 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.  ) ) ) )
4746exbidv 1779 . . . 4  |-  ( 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.  ) ) ) )
4814, 47anbi12d 722 . . 3  |-  ( 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 32787 . . 3  |-  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 ) ) ) ) }
5048, 49elrab2 3210 . 2  |-  ( 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 659 . 2  |-  ( ( ( 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 995 . . . 4  |-  ( ( K  e.  Poset  /\  B  e.  dom  U  /\  B  e.  dom  G )  <->  ( K  e.  Poset  /\  ( B  e.  dom  U  /\  B  e.  dom  G ) ) )
5352bicomi 207 . . 3  |-  ( ( K  e.  Poset  /\  ( B  e.  dom  U  /\  B  e.  dom  G ) )  <->  ( K  e. 
Poset  /\  B  e.  dom  U  /\  B  e.  dom  G ) )
54 fvex 5898 . . . . 5  |-  ( oc
`  K )  e. 
_V
5516, 54eqeltri 2536 . . . 4  |-  ._|_  e.  _V
56 fveq1 5887 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 x )  =  (  ._|_  `  x ) )
5756eleq1d 2524 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  x )  e.  B  <->  (  ._|_  `  x )  e.  B
) )
58 id 22 . . . . . . . . 9  |-  ( n  =  ._|_  ->  n  = 
._|_  )
5958, 56fveq12d 5894 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 ( n `  x ) )  =  (  ._|_  `  (  ._|_  `  x ) ) )
6059eqeq1d 2464 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  ( n `
 x ) )  =  x  <->  (  ._|_  `  (  ._|_  `  x ) )  =  x ) )
61 fveq1 5887 . . . . . . . . 9  |-  ( n  =  ._|_  ->  ( n `
 y )  =  (  ._|_  `  y ) )
6261, 56breq12d 4429 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( ( n `  y ) 
.<_  ( n `  x
)  <->  (  ._|_  `  y
)  .<_  (  ._|_  `  x
) ) )
6362imbi2d 322 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( x  .<_  y  ->  ( n `  y ) 
.<_  ( n `  x
) )  <->  ( x  .<_  y  ->  (  ._|_  `  y )  .<_  (  ._|_  `  x ) ) ) )
6457, 60, 633anbi123d 1348 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( ( n `  x
)  e.  B  /\  ( n `  (
n `  x )
)  =  x  /\  ( x  .<_  y  -> 
( n `  y
)  .<_  ( n `  x ) ) )  <-> 
( (  ._|_  `  x
)  e.  B  /\  (  ._|_  `  (  ._|_  `  x ) )  =  x  /\  ( x 
.<_  y  ->  (  ._|_  `  y )  .<_  (  ._|_  `  x ) ) ) ) )
6556oveq2d 6331 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
.\/  ( n `  x ) )  =  ( x  .\/  (  ._|_  `  x ) ) )
6665eqeq1d 2464 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  .\/  ( n `
 x ) )  =  .1.  <->  ( x  .\/  (  ._|_  `  x
) )  =  .1.  ) )
6756oveq2d 6331 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
./\  ( n `  x ) )  =  ( x  ./\  (  ._|_  `  x ) ) )
6867eqeq1d 2464 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  ./\  ( n `  x ) )  =  .0.  <->  ( x  ./\  (  ._|_  `  x )
)  =  .0.  )
)
6964, 66, 683anbi123d 1348 . . . . 5  |-  ( 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.  ) ) )
70692ralbidv 2844 . . . 4  |-  ( 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.  ) ) )
7155, 70ceqsexv 3096 . . 3  |-  ( 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.  ) )
7253, 71anbi12i 708 . 2  |-  ( ( ( 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.  ) ) )
7350, 51, 723bitr2i 281 1  |-  ( 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.  ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    /\ w3a 991    = wceq 1455   E.wex 1674    e. wcel 1898   A.wral 2749   _Vcvv 3057   class class class wbr 4416   dom cdm 4853   ` cfv 5601  (class class class)co 6315   Basecbs 15170   lecple 15246   occoc 15247   Posetcpo 16234   lubclub 16236   glbcglb 16237   joincjn 16238   meetcmee 16239   0.cp0 16332   1.cp1 16333   OPcops 32783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-nul 4548
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-dm 4863  df-iota 5565  df-fv 5609  df-ov 6318  df-oposet 32787
This theorem is referenced by:  opposet  32792  oposlem  32793  op01dm  32794
  Copyright terms: Public domain W3C validator