Metamath Proof Explorer

Theorem op01dm

Description: Conditions necessary for zero and unity elements to exist. (Contributed by NM, 14-Sep-2018)

Ref Expression
Hypotheses op01dm.b ⊢B=BaseK
op01dm.u ⊢U=lub⁡K
op01dm.g ⊢G=glb⁡K
Assertion op01dm ⊢K∈OP→B∈dom⁡U∧B∈dom⁡G

Proof

Step Hyp Ref Expression
1 op01dm.b ⊢B=BaseK
2 op01dm.u ⊢U=lub⁡K
3 op01dm.g ⊢G=glb⁡K
4 eqid ⊢≤K=≤K
5 eqid ⊢oc⁡K=oc⁡K
6 eqid ⊢join⁡K=join⁡K
7 eqid ⊢meet⁡K=meet⁡K
8 eqid ⊢0.⁡K=0.⁡K
9 eqid ⊢1.⁡K=1.⁡K
10 1 2 3 4 5 6 7 8 9 isopos ⊢K∈OP↔K∈Poset∧B∈dom⁡U∧B∈dom⁡G∧∀x∈B∀y∈Boc⁡K⁡x∈B∧oc⁡K⁡oc⁡K⁡x=x∧x≤Ky→oc⁡K⁡y≤Koc⁡K⁡x∧xjoin⁡Koc⁡K⁡x=1.⁡K∧xmeet⁡Koc⁡K⁡x=0.⁡K
11 simpl ⊢B∈dom⁡U∧B∈dom⁡G∧∀x∈B∀y∈Boc⁡K⁡x∈B∧oc⁡K⁡oc⁡K⁡x=x∧x≤Ky→oc⁡K⁡y≤Koc⁡K⁡x∧xjoin⁡Koc⁡K⁡x=1.⁡K∧xmeet⁡Koc⁡K⁡x=0.⁡K→B∈dom⁡U∧B∈dom⁡G
12 11 3adantl1 ⊢K∈Poset∧B∈dom⁡U∧B∈dom⁡G∧∀x∈B∀y∈Boc⁡K⁡x∈B∧oc⁡K⁡oc⁡K⁡x=x∧x≤Ky→oc⁡K⁡y≤Koc⁡K⁡x∧xjoin⁡Koc⁡K⁡x=1.⁡K∧xmeet⁡Koc⁡K⁡x=0.⁡K→B∈dom⁡U∧B∈dom⁡G
13 10 12 sylbi ⊢K∈OP→B∈dom⁡U∧B∈dom⁡G