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