Theorem op01dm 39169

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

Hypotheses

Ref	Expression
op01dm.b	⊢ 𝐵 = (Base‘𝐾)
op01dm.u	⊢ 𝑈 = (lub‘𝐾)
op01dm.g	⊢ 𝐺 = (glb‘𝐾)

Assertion

Ref	Expression
op01dm	⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))

Proof of Theorem op01dm

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		op01dm.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		op01dm.u	. . 3 ⊢ 𝑈 = (lub‘𝐾)
3		op01dm.g	. . 3 ⊢ 𝐺 = (glb‘𝐾)
4		eqid 2729	. . 3 ⊢ (le‘𝐾) = (le‘𝐾)
5		eqid 2729	. . 3 ⊢ (oc‘𝐾) = (oc‘𝐾)
6		eqid 2729	. . 3 ⊢ (join‘𝐾) = (join‘𝐾)
7		eqid 2729	. . 3 ⊢ (meet‘𝐾) = (meet‘𝐾)
8		eqid 2729	. . 3 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2729	. . 3 ⊢ (1.‘𝐾) = (1.‘𝐾)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	isopos 39166	. 2 ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))))
11		simpl 482	. . 3 ⊢ (((𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))
12	11	3adantl1 1167	. 2 ⊢ (((𝐾 ∈ Poset ∧ 𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((((oc‘𝐾)‘𝑥) ∈ 𝐵 ∧ ((oc‘𝐾)‘((oc‘𝐾)‘𝑥)) = 𝑥 ∧ (𝑥(le‘𝐾)𝑦 → ((oc‘𝐾)‘𝑦)(le‘𝐾)((oc‘𝐾)‘𝑥))) ∧ (𝑥(join‘𝐾)((oc‘𝐾)‘𝑥)) = (1.‘𝐾) ∧ (𝑥(meet‘𝐾)((oc‘𝐾)‘𝑥)) = (0.‘𝐾))) → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))
13	10, 12	sylbi 217	1 ⊢ (𝐾 ∈ OP → (𝐵 ∈ dom 𝑈 ∧ 𝐵 ∈ dom 𝐺))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044   class class class wbr 5102  dom cdm 5631  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  lecple 17203  occoc 17204  Posetcpo 18248  lubclub 18250  glbcglb 18251  joincjn 18252  meetcmee 18253  0.cp0 18362  1.cp1 18363  OPcops 39158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-dm 5641  df-iota 6452  df-fv 6507  df-ov 7372  df-oposet 39162

This theorem is referenced by:  op0cl  39170  op1cl  39171  op0le  39172  ople1  39177  lhp2lt  39988