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

Theorem isopos 32825
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 5691 . . . . . . 7  |-  ( p  =  K  ->  ( Base `  p )  =  ( Base `  K
) )
2 isopos.b . . . . . . 7  |-  B  =  ( Base `  K
)
31, 2syl6eqr 2493 . . . . . 6  |-  ( p  =  K  ->  ( Base `  p )  =  B )
4 fveq2 5691 . . . . . . . 8  |-  ( p  =  K  ->  ( lub `  p )  =  ( lub `  K
) )
5 isopos.e . . . . . . . 8  |-  U  =  ( lub `  K
)
64, 5syl6eqr 2493 . . . . . . 7  |-  ( p  =  K  ->  ( lub `  p )  =  U )
76dmeqd 5042 . . . . . 6  |-  ( p  =  K  ->  dom  ( lub `  p )  =  dom  U )
83, 7eleq12d 2511 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( lub `  p
)  <->  B  e.  dom  U ) )
9 fveq2 5691 . . . . . . . 8  |-  ( p  =  K  ->  ( glb `  p )  =  ( glb `  K
) )
10 isopos.g . . . . . . . 8  |-  G  =  ( glb `  K
)
119, 10syl6eqr 2493 . . . . . . 7  |-  ( p  =  K  ->  ( glb `  p )  =  G )
1211dmeqd 5042 . . . . . 6  |-  ( p  =  K  ->  dom  ( glb `  p )  =  dom  G )
133, 12eleq12d 2511 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( glb `  p
)  <->  B  e.  dom  G ) )
148, 13anbi12d 710 . . . 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 5691 . . . . . . . 8  |-  ( p  =  K  ->  ( oc `  p )  =  ( oc `  K
) )
16 isopos.o . . . . . . . 8  |-  ._|_  =  ( oc `  K )
1715, 16syl6eqr 2493 . . . . . . 7  |-  ( p  =  K  ->  ( oc `  p )  = 
._|_  )
1817eqeq2d 2454 . . . . . 6  |-  ( p  =  K  ->  (
n  =  ( oc
`  p )  <->  n  =  ._|_  ) )
193eleq2d 2510 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( n `  x
)  e.  ( Base `  p )  <->  ( n `  x )  e.  B
) )
20 fveq2 5691 . . . . . . . . . . . . 13  |-  ( p  =  K  ->  ( le `  p )  =  ( le `  K
) )
21 isopos.l . . . . . . . . . . . . 13  |-  .<_  =  ( le `  K )
2220, 21syl6eqr 2493 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( le `  p )  = 
.<_  )
2322breqd 4303 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
x ( le `  p ) y  <->  x  .<_  y ) )
2422breqd 4303 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
( n `  y
) ( le `  p ) ( n `
 x )  <->  ( n `  y )  .<_  ( n `
 x ) ) )
2523, 24imbi12d 320 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( x ( le
`  p ) y  ->  ( n `  y ) ( le
`  p ) ( n `  x ) )  <->  ( x  .<_  y  ->  ( n `  y )  .<_  ( n `
 x ) ) ) )
2619, 253anbi13d 1291 . . . . . . . . 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 5691 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( join `  p )  =  ( join `  K
) )
28 isopos.j . . . . . . . . . . . 12  |-  .\/  =  ( join `  K )
2927, 28syl6eqr 2493 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( join `  p )  = 
.\/  )
3029oveqd 6108 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( join `  p
) ( n `  x ) )  =  ( x  .\/  (
n `  x )
) )
31 fveq2 5691 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 1. `  p )  =  ( 1. `  K
) )
32 isopos.u . . . . . . . . . . 11  |-  .1.  =  ( 1. `  K )
3331, 32syl6eqr 2493 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 1. `  p )  =  .1.  )
3430, 33eqeq12d 2457 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( join `  p ) ( n `
 x ) )  =  ( 1. `  p )  <->  ( x  .\/  ( n `  x
) )  =  .1.  ) )
35 fveq2 5691 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( meet `  p )  =  ( meet `  K
) )
36 isopos.m . . . . . . . . . . . 12  |-  ./\  =  ( meet `  K )
3735, 36syl6eqr 2493 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( meet `  p )  = 
./\  )
3837oveqd 6108 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( meet `  p
) ( n `  x ) )  =  ( x  ./\  (
n `  x )
) )
39 fveq2 5691 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 0. `  p )  =  ( 0. `  K
) )
40 isopos.f . . . . . . . . . . 11  |-  .0.  =  ( 0. `  K )
4139, 40syl6eqr 2493 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 0. `  p )  =  .0.  )
4238, 41eqeq12d 2457 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( meet `  p ) ( n `
 x ) )  =  ( 0. `  p )  <->  ( x  ./\  ( n `  x
) )  =  .0.  ) )
4326, 34, 423anbi123d 1289 . . . . . . . 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 2931 . . . . . . 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 2931 . . . . . 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 710 . . . . 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 1680 . . . 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 710 . . 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 32821 . . 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 3119 . 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 649 . 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 969 . . . 4  |-  ( ( K  e.  Poset  /\  B  e.  dom  U  /\  B  e.  dom  G )  <->  ( K  e.  Poset  /\  ( B  e.  dom  U  /\  B  e.  dom  G ) ) )
5352bicomi 202 . . 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 5701 . . . . 5  |-  ( oc
`  K )  e. 
_V
5516, 54eqeltri 2513 . . . 4  |-  ._|_  e.  _V
56 fveq1 5690 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 x )  =  (  ._|_  `  x ) )
5756eleq1d 2509 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  x )  e.  B  <->  (  ._|_  `  x )  e.  B
) )
58 id 22 . . . . . . . . 9  |-  ( n  =  ._|_  ->  n  = 
._|_  )
5958, 56fveq12d 5697 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 ( n `  x ) )  =  (  ._|_  `  (  ._|_  `  x ) ) )
6059eqeq1d 2451 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  ( n `
 x ) )  =  x  <->  (  ._|_  `  (  ._|_  `  x ) )  =  x ) )
61 fveq1 5690 . . . . . . . . 9  |-  ( n  =  ._|_  ->  ( n `
 y )  =  (  ._|_  `  y ) )
6261, 56breq12d 4305 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( ( n `  y ) 
.<_  ( n `  x
)  <->  (  ._|_  `  y
)  .<_  (  ._|_  `  x
) ) )
6362imbi2d 316 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( x  .<_  y  ->  ( n `  y ) 
.<_  ( n `  x
) )  <->  ( x  .<_  y  ->  (  ._|_  `  y )  .<_  (  ._|_  `  x ) ) ) )
6457, 60, 633anbi123d 1289 . . . . . 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 6107 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
.\/  ( n `  x ) )  =  ( x  .\/  (  ._|_  `  x ) ) )
6665eqeq1d 2451 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  .\/  ( n `
 x ) )  =  .1.  <->  ( x  .\/  (  ._|_  `  x
) )  =  .1.  ) )
6756oveq2d 6107 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
./\  ( n `  x ) )  =  ( x  ./\  (  ._|_  `  x ) ) )
6867eqeq1d 2451 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  ./\  ( n `  x ) )  =  .0.  <->  ( x  ./\  (  ._|_  `  x )
)  =  .0.  )
)
6964, 66, 683anbi123d 1289 . . . . 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 2757 . . . 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 3009 . . 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 697 . 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 273 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 184    /\ wa 369    /\ w3a 965    = wceq 1369   E.wex 1586    e. wcel 1756   A.wral 2715   _Vcvv 2972   class class class wbr 4292   dom cdm 4840   ` cfv 5418  (class class class)co 6091   Basecbs 14174   lecple 14245   occoc 14246   Posetcpo 15110   lubclub 15112   glbcglb 15113   joincjn 15114   meetcmee 15115   0.cp0 15207   1.cp1 15208   OPcops 32817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-dm 4850  df-iota 5381  df-fv 5426  df-ov 6094  df-oposet 32821
This theorem is referenced by:  opposet  32826  oposlem  32827  op01dm  32828
  Copyright terms: Public domain W3C validator