# Metamath Proof Explorer

## Theorem isopos

Description: The predicate "is an orthoposet." (Contributed by NM, 20-Oct-2011) (Revised by NM, 14-Sep-2018)

Ref Expression
Hypotheses isopos.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
isopos.e ${⊢}{U}=\mathrm{lub}\left({K}\right)$
isopos.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
isopos.l
isopos.o
isopos.j
isopos.m
isopos.f
isopos.u
Assertion isopos

### Proof

Step Hyp Ref Expression
1 isopos.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 isopos.e ${⊢}{U}=\mathrm{lub}\left({K}\right)$
3 isopos.g ${⊢}{G}=\mathrm{glb}\left({K}\right)$
4 isopos.l
5 isopos.o
6 isopos.j
7 isopos.m
8 isopos.f
9 isopos.u
10 fveq2 ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={\mathrm{Base}}_{{K}}$
11 10 1 eqtr4di ${⊢}{p}={K}\to {\mathrm{Base}}_{{p}}={B}$
12 fveq2 ${⊢}{p}={K}\to \mathrm{lub}\left({p}\right)=\mathrm{lub}\left({K}\right)$
13 12 2 eqtr4di ${⊢}{p}={K}\to \mathrm{lub}\left({p}\right)={U}$
14 13 dmeqd ${⊢}{p}={K}\to \mathrm{dom}\mathrm{lub}\left({p}\right)=\mathrm{dom}{U}$
15 11 14 eleq12d ${⊢}{p}={K}\to \left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)↔{B}\in \mathrm{dom}{U}\right)$
16 fveq2 ${⊢}{p}={K}\to \mathrm{glb}\left({p}\right)=\mathrm{glb}\left({K}\right)$
17 16 3 eqtr4di ${⊢}{p}={K}\to \mathrm{glb}\left({p}\right)={G}$
18 17 dmeqd ${⊢}{p}={K}\to \mathrm{dom}\mathrm{glb}\left({p}\right)=\mathrm{dom}{G}$
19 11 18 eleq12d ${⊢}{p}={K}\to \left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)↔{B}\in \mathrm{dom}{G}\right)$
20 15 19 anbi12d ${⊢}{p}={K}\to \left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)↔\left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\right)$
21 fveq2 ${⊢}{p}={K}\to \mathrm{oc}\left({p}\right)=\mathrm{oc}\left({K}\right)$
22 21 5 eqtr4di
23 22 eqeq2d
24 11 eleq2d ${⊢}{p}={K}\to \left({n}\left({x}\right)\in {\mathrm{Base}}_{{p}}↔{n}\left({x}\right)\in {B}\right)$
25 fveq2 ${⊢}{p}={K}\to {\le }_{{p}}={\le }_{{K}}$
26 25 4 eqtr4di
27 26 breqd
28 26 breqd
29 27 28 imbi12d
30 24 29 3anbi13d
31 fveq2 ${⊢}{p}={K}\to \mathrm{join}\left({p}\right)=\mathrm{join}\left({K}\right)$
32 31 6 eqtr4di
33 32 oveqd
34 fveq2 ${⊢}{p}={K}\to \mathrm{1.}\left({p}\right)=\mathrm{1.}\left({K}\right)$
35 34 9 eqtr4di
36 33 35 eqeq12d
37 fveq2 ${⊢}{p}={K}\to \mathrm{meet}\left({p}\right)=\mathrm{meet}\left({K}\right)$
38 37 7 eqtr4di
39 38 oveqd
40 fveq2 ${⊢}{p}={K}\to \mathrm{0.}\left({p}\right)=\mathrm{0.}\left({K}\right)$
41 40 8 eqtr4di
42 39 41 eqeq12d
43 30 36 42 3anbi123d
44 11 43 raleqbidv
45 11 44 raleqbidv
46 23 45 anbi12d
47 46 exbidv
48 20 47 anbi12d
49 df-oposet ${⊢}\mathrm{OP}=\left\{{p}\in \mathrm{Poset}|\left(\left({\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{lub}\left({p}\right)\wedge {\mathrm{Base}}_{{p}}\in \mathrm{dom}\mathrm{glb}\left({p}\right)\right)\wedge \exists {n}\phantom{\rule{.4em}{0ex}}\left({n}=\mathrm{oc}\left({p}\right)\wedge \forall {x}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{p}}\phantom{\rule{.4em}{0ex}}\left(\left({n}\left({x}\right)\in {\mathrm{Base}}_{{p}}\wedge {n}\left({n}\left({x}\right)\right)={x}\wedge \left({x}{\le }_{{p}}{y}\to {n}\left({y}\right){\le }_{{p}}{n}\left({x}\right)\right)\right)\wedge {x}\mathrm{join}\left({p}\right){n}\left({x}\right)=\mathrm{1.}\left({p}\right)\wedge {x}\mathrm{meet}\left({p}\right){n}\left({x}\right)=\mathrm{0.}\left({p}\right)\right)\right)\right)\right\}$
50 48 49 elrab2
51 anass
52 3anass ${⊢}\left({K}\in \mathrm{Poset}\wedge {B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)↔\left({K}\in \mathrm{Poset}\wedge \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\right)$
53 52 bicomi ${⊢}\left({K}\in \mathrm{Poset}\wedge \left({B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)\right)↔\left({K}\in \mathrm{Poset}\wedge {B}\in \mathrm{dom}{U}\wedge {B}\in \mathrm{dom}{G}\right)$
54 5 fvexi
55 fveq1
56 55 eleq1d
57 id
58 57 55 fveq12d
59 58 eqeq1d
60 fveq1
61 60 55 breq12d
62 61 imbi2d
63 56 59 62 3anbi123d
64 55 oveq2d
65 64 eqeq1d
66 55 oveq2d
67 66 eqeq1d
68 63 65 67 3anbi123d
69 68 2ralbidv
70 54 69 ceqsexv
71 53 70 anbi12i
72 50 51 71 3bitr2i