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

Theorem isopos 35048
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 5872 . . . . . . 7  |-  ( p  =  K  ->  ( Base `  p )  =  ( Base `  K
) )
2 isopos.b . . . . . . 7  |-  B  =  ( Base `  K
)
31, 2syl6eqr 2516 . . . . . 6  |-  ( p  =  K  ->  ( Base `  p )  =  B )
4 fveq2 5872 . . . . . . . 8  |-  ( p  =  K  ->  ( lub `  p )  =  ( lub `  K
) )
5 isopos.e . . . . . . . 8  |-  U  =  ( lub `  K
)
64, 5syl6eqr 2516 . . . . . . 7  |-  ( p  =  K  ->  ( lub `  p )  =  U )
76dmeqd 5215 . . . . . 6  |-  ( p  =  K  ->  dom  ( lub `  p )  =  dom  U )
83, 7eleq12d 2539 . . . . 5  |-  ( p  =  K  ->  (
( Base `  p )  e.  dom  ( lub `  p
)  <->  B  e.  dom  U ) )
9 fveq2 5872 . . . . . . . 8  |-  ( p  =  K  ->  ( glb `  p )  =  ( glb `  K
) )
10 isopos.g . . . . . . . 8  |-  G  =  ( glb `  K
)
119, 10syl6eqr 2516 . . . . . . 7  |-  ( p  =  K  ->  ( glb `  p )  =  G )
1211dmeqd 5215 . . . . . 6  |-  ( p  =  K  ->  dom  ( glb `  p )  =  dom  G )
133, 12eleq12d 2539 . . . . 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 5872 . . . . . . . 8  |-  ( p  =  K  ->  ( oc `  p )  =  ( oc `  K
) )
16 isopos.o . . . . . . . 8  |-  ._|_  =  ( oc `  K )
1715, 16syl6eqr 2516 . . . . . . 7  |-  ( p  =  K  ->  ( oc `  p )  = 
._|_  )
1817eqeq2d 2471 . . . . . 6  |-  ( p  =  K  ->  (
n  =  ( oc
`  p )  <->  n  =  ._|_  ) )
193eleq2d 2527 . . . . . . . . . 10  |-  ( p  =  K  ->  (
( n `  x
)  e.  ( Base `  p )  <->  ( n `  x )  e.  B
) )
20 fveq2 5872 . . . . . . . . . . . . 13  |-  ( p  =  K  ->  ( le `  p )  =  ( le `  K
) )
21 isopos.l . . . . . . . . . . . . 13  |-  .<_  =  ( le `  K )
2220, 21syl6eqr 2516 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( le `  p )  = 
.<_  )
2322breqd 4467 . . . . . . . . . . 11  |-  ( p  =  K  ->  (
x ( le `  p ) y  <->  x  .<_  y ) )
2422breqd 4467 . . . . . . . . . . 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 1301 . . . . . . . . 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 5872 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( join `  p )  =  ( join `  K
) )
28 isopos.j . . . . . . . . . . . 12  |-  .\/  =  ( join `  K )
2927, 28syl6eqr 2516 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( join `  p )  = 
.\/  )
3029oveqd 6313 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( join `  p
) ( n `  x ) )  =  ( x  .\/  (
n `  x )
) )
31 fveq2 5872 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 1. `  p )  =  ( 1. `  K
) )
32 isopos.u . . . . . . . . . . 11  |-  .1.  =  ( 1. `  K )
3331, 32syl6eqr 2516 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 1. `  p )  =  .1.  )
3430, 33eqeq12d 2479 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( join `  p ) ( n `
 x ) )  =  ( 1. `  p )  <->  ( x  .\/  ( n `  x
) )  =  .1.  ) )
35 fveq2 5872 . . . . . . . . . . . 12  |-  ( p  =  K  ->  ( meet `  p )  =  ( meet `  K
) )
36 isopos.m . . . . . . . . . . . 12  |-  ./\  =  ( meet `  K )
3735, 36syl6eqr 2516 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( meet `  p )  = 
./\  )
3837oveqd 6313 . . . . . . . . . 10  |-  ( p  =  K  ->  (
x ( meet `  p
) ( n `  x ) )  =  ( x  ./\  (
n `  x )
) )
39 fveq2 5872 . . . . . . . . . . 11  |-  ( p  =  K  ->  ( 0. `  p )  =  ( 0. `  K
) )
40 isopos.f . . . . . . . . . . 11  |-  .0.  =  ( 0. `  K )
4139, 40syl6eqr 2516 . . . . . . . . . 10  |-  ( p  =  K  ->  ( 0. `  p )  =  .0.  )
4238, 41eqeq12d 2479 . . . . . . . . 9  |-  ( p  =  K  ->  (
( x ( meet `  p ) ( n `
 x ) )  =  ( 0. `  p )  <->  ( x  ./\  ( n `  x
) )  =  .0.  ) )
4326, 34, 423anbi123d 1299 . . . . . . . 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 3068 . . . . . . 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 3068 . . . . . 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 1715 . . . 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 35044 . . 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 3259 . 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 977 . . . 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 5882 . . . . 5  |-  ( oc
`  K )  e. 
_V
5516, 54eqeltri 2541 . . . 4  |-  ._|_  e.  _V
56 fveq1 5871 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 x )  =  (  ._|_  `  x ) )
5756eleq1d 2526 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  x )  e.  B  <->  (  ._|_  `  x )  e.  B
) )
58 id 22 . . . . . . . . 9  |-  ( n  =  ._|_  ->  n  = 
._|_  )
5958, 56fveq12d 5878 . . . . . . . 8  |-  ( n  =  ._|_  ->  ( n `
 ( n `  x ) )  =  (  ._|_  `  (  ._|_  `  x ) ) )
6059eqeq1d 2459 . . . . . . 7  |-  ( n  =  ._|_  ->  ( ( n `  ( n `
 x ) )  =  x  <->  (  ._|_  `  (  ._|_  `  x ) )  =  x ) )
61 fveq1 5871 . . . . . . . . 9  |-  ( n  =  ._|_  ->  ( n `
 y )  =  (  ._|_  `  y ) )
6261, 56breq12d 4469 . . . . . . . 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 1299 . . . . . 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 6312 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
.\/  ( n `  x ) )  =  ( x  .\/  (  ._|_  `  x ) ) )
6665eqeq1d 2459 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  .\/  ( n `
 x ) )  =  .1.  <->  ( x  .\/  (  ._|_  `  x
) )  =  .1.  ) )
6756oveq2d 6312 . . . . . . 7  |-  ( n  =  ._|_  ->  ( x 
./\  ( n `  x ) )  =  ( x  ./\  (  ._|_  `  x ) ) )
6867eqeq1d 2459 . . . . . 6  |-  ( n  =  ._|_  ->  ( ( x  ./\  ( n `  x ) )  =  .0.  <->  ( x  ./\  (  ._|_  `  x )
)  =  .0.  )
)
6964, 66, 683anbi123d 1299 . . . . 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 2901 . . . 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 3146 . . 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 973    = wceq 1395   E.wex 1613    e. wcel 1819   A.wral 2807   _Vcvv 3109   class class class wbr 4456   dom cdm 5008   ` cfv 5594  (class class class)co 6296   Basecbs 14644   lecple 14719   occoc 14720   Posetcpo 15696   lubclub 15698   glbcglb 15699   joincjn 15700   meetcmee 15701   0.cp0 15794   1.cp1 15795   OPcops 35040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-nul 4586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-dm 5018  df-iota 5557  df-fv 5602  df-ov 6299  df-oposet 35044
This theorem is referenced by:  opposet  35049  oposlem  35050  op01dm  35051
  Copyright terms: Public domain W3C validator