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 = Base K
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 = Base K
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 ∈ B oc ⁡ K ⁡ x ∈ B ∧ oc ⁡ K ⁡ oc ⁡ K ⁡ x = x ∧ x ≤ K y → oc ⁡ K ⁡ y ≤ K oc ⁡ K ⁡ x ∧ x join ⁡ K oc ⁡ K ⁡ x = 1. ⁡ K ∧ x meet ⁡ K oc ⁡ K ⁡ x = 0. ⁡ K
11 simpl ⊢ B ∈ dom ⁡ U ∧ B ∈ dom ⁡ G ∧ ∀ x ∈ B ∀ y ∈ B oc ⁡ K ⁡ x ∈ B ∧ oc ⁡ K ⁡ oc ⁡ K ⁡ x = x ∧ x ≤ K y → oc ⁡ K ⁡ y ≤ K oc ⁡ K ⁡ x ∧ x join ⁡ K oc ⁡ K ⁡ x = 1. ⁡ K ∧ x meet ⁡ K oc ⁡ K ⁡ x = 0. ⁡ K → B ∈ dom ⁡ U ∧ B ∈ dom ⁡ G
12 11 3adantl1 ⊢ K ∈ Poset ∧ B ∈ dom ⁡ U ∧ B ∈ dom ⁡ G ∧ ∀ x ∈ B ∀ y ∈ B oc ⁡ K ⁡ x ∈ B ∧ oc ⁡ K ⁡ oc ⁡ K ⁡ x = x ∧ x ≤ K y → oc ⁡ K ⁡ y ≤ K oc ⁡ K ⁡ x ∧ x join ⁡ K oc ⁡ K ⁡ x = 1. ⁡ K ∧ x meet ⁡ K oc ⁡ K ⁡ x = 0. ⁡ K → B ∈ dom ⁡ U ∧ B ∈ dom ⁡ G
13 10 12 sylbi ⊢ K ∈ OP → B ∈ dom ⁡ U ∧ B ∈ dom ⁡ G