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

Theorem isopos 32513
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 5688 . . . . . . 7  |-  ( p  =  K  ->  ( Base `  p )  =  ( Base `  K
) )
2 isopos.b . . . . . . 7  |-  B  =  ( Base `  K
)
31, 2syl6eqr 2491 . . . . . 6  |-  ( p  =  K  ->  ( Base `  p )  =  B )
4 fveq2 5688 . . . . . . . 8  |-  ( p  =  K  ->  ( lub `  p )  =  ( lub `  K
) )
5 isopos.e . . . . . . . 8  |-  U  =  ( lub `  K
)
64, 5syl6eqr 2491 . . . . . . 7  |-  ( p  =  K  ->  ( lub `  p )  =  U )
76dmeqd 5038 . . . . . 6  |-  ( p  =  K  ->  dom  ( lub `  p )  =  dom  U )
83, 7eleq12d 2509 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( lub `  p
)  <->  B  e.  dom  U ) )
9 fveq2 5688 . . . . . . . 8  |-  ( p  =  K  ->  ( glb `  p )  =  ( glb `  K
) )
10 isopos.g . . . . . . . 8  |-  G  =  ( glb `  K
)
119, 10syl6eqr 2491 . . . . . . 7  |-  ( p  =  K  ->  ( glb `  p )  =  G )
1211dmeqd 5038 . . . . . 6  |-  ( p  =  K  ->  dom  ( glb `  p )  =  dom  G )
133, 12eleq12d 2509 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( glb `  p
)  <->  B  e.  dom  G ) )
148, 13anbi12d 705 . . . 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 5688 . . . . . . . 8  |-  ( p  =  K  ->  ( oc `  p )  =  ( oc `  K
) )
16 isopos.o . . . . . . . 8  |-  ._|_  =  ( oc `  K )
1715, 16syl6eqr 2491 . . . . . . 7  |-  ( p  =  K  ->  ( oc `  p )  = 
._|_  )
1817eqeq2d 2452 . . . . . 6  |-  ( p  =  K  ->  (
n  =  ( oc
`  p )  <->  n  =  ._|_  ) )
193eleq2d 2508 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( n `  x
)  e.  ( Base `  p )  <->  ( n `  x )  e.  B
) )
20 fveq2 5688 . . . . . . . . . . . . 13  |-  ( p  =  K  ->  ( le `  p )  =  ( le `  K
) )
21 isopos.l . . . . . . . . . . . . 13  |-  .<_  =  ( le `  K )
2220, 21syl6eqr 2491 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( le `  p )  = 
.<_  )
2322breqd 4300 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
x ( le `  p ) y  <->  x  .<_  y ) )
2422breqd 4300 . . . . . . . . . . 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 1286 . . . . . . . . 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 5688 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( join `  p )  =  ( join `  K
) )
28 isopos.j . . . . . . . . . . . 12  |-  .\/  =  ( join `  K )
2927, 28syl6eqr 2491 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( join `  p )  = 
.\/  )
3029oveqd 6107 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( join `  p
) ( n `  x ) )  =  ( x  .\/  (
n `  x )
) )
31 fveq2 5688 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 1. `  p )  =  ( 1. `  K
) )
32 isopos.u . . . . . . . . . . 11  |-  .1.  =  ( 1. `  K )
3331, 32syl6eqr 2491 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 1. `  p )  =  .1.  )
3430, 33eqeq12d 2455 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( join `  p ) ( n `
 x ) )  =  ( 1. `  p )  <->  ( x  .\/  ( n `  x
) )  =  .1.  ) )
35 fveq2 5688 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( meet `  p )  =  ( meet `  K
) )
36 isopos.m . . . . . . . . . . . 12  |-  ./\  =  ( meet `  K )
3735, 36syl6eqr 2491 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( meet `  p )  = 
./\  )
3837oveqd 6107 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( meet `  p
) ( n `  x ) )  =  ( x  ./\  (
n `  x )
) )
39 fveq2 5688 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 0. `  p )  =  ( 0. `  K
) )
40 isopos.f . . . . . . . . . . 11  |-  .0.  =  ( 0. `  K )
4139, 40syl6eqr 2491 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 0. `  p )  =  .0.  )
4238, 41eqeq12d 2455 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( meet `  p ) ( n `
 x ) )  =  ( 0. `  p )  <->  ( x  ./\  ( n `  x
) )  =  .0.  ) )
4326, 34, 423anbi123d 1284 . . . . . . . 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 2929 . . . . . . 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 2929 . . . . . 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 705 . . . . 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 1685 . . . 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 705 . . 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 32509 . . 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 3116 . 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 644 . 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 964 . . . 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 5698 . . . . 5  |-  ( oc
`  K )  e. 
_V
5516, 54eqeltri 2511 . . . 4  |-  ._|_  e.  _V
56 fveq1 5687 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 x )  =  (  ._|_  `  x ) )
5756eleq1d 2507 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  x )  e.  B  <->  (  ._|_  `  x )  e.  B
) )
58 id 22 . . . . . . . . 9  |-  ( n  =  ._|_  ->  n  = 
._|_  )
5958, 56fveq12d 5694 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 ( n `  x ) )  =  (  ._|_  `  (  ._|_  `  x ) ) )
6059eqeq1d 2449 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  ( n `
 x ) )  =  x  <->  (  ._|_  `  (  ._|_  `  x ) )  =  x ) )
61 fveq1 5687 . . . . . . . . 9  |-  ( n  =  ._|_  ->  ( n `
 y )  =  (  ._|_  `  y ) )
6261, 56breq12d 4302 . . . . . . . 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 1284 . . . . . 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 6106 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
.\/  ( n `  x ) )  =  ( x  .\/  (  ._|_  `  x ) ) )
6665eqeq1d 2449 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  .\/  ( n `
 x ) )  =  .1.  <->  ( x  .\/  (  ._|_  `  x
) )  =  .1.  ) )
6756oveq2d 6106 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
./\  ( n `  x ) )  =  ( x  ./\  (  ._|_  `  x ) ) )
6867eqeq1d 2449 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  ./\  ( n `  x ) )  =  .0.  <->  ( x  ./\  (  ._|_  `  x )
)  =  .0.  )
)
6964, 66, 683anbi123d 1284 . . . . 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 2755 . . . 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 3006 . . 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 692 . 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 960    = wceq 1364   E.wex 1591    e. wcel 1761   A.wral 2713   _Vcvv 2970   class class class wbr 4289   dom cdm 4836   ` cfv 5415  (class class class)co 6090   Basecbs 14170   lecple 14241   occoc 14242   Posetcpo 15106   lubclub 15108   glbcglb 15109   joincjn 15110   meetcmee 15111   0.cp0 15203   1.cp1 15204   OPcops 32505
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-nul 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-dm 4846  df-iota 5378  df-fv 5423  df-ov 6093  df-oposet 32509
This theorem is referenced by:  opposet  32514  oposlem  32515  op01dm  32516
  Copyright terms: Public domain W3C validator