Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  glb0N Structured version   Visualization version   GIF version

Theorem glb0N 37134
Description: The greatest lower bound of the empty set is the unit element. (Contributed by NM, 5-Dec-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
glb0.g 𝐺 = (glb‘𝐾)
glb0.u 1 = (1.‘𝐾)
Assertion
Ref Expression
glb0N (𝐾 ∈ OP → (𝐺‘∅) = 1 )

Proof of Theorem glb0N
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2738 . . 3 (le‘𝐾) = (le‘𝐾)
3 glb0.g . . 3 𝐺 = (glb‘𝐾)
4 biid 260 . . 3 ((∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥)) ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥)))
5 id 22 . . 3 (𝐾 ∈ OP → 𝐾 ∈ OP)
6 0ss 4327 . . . 4 ∅ ⊆ (Base‘𝐾)
76a1i 11 . . 3 (𝐾 ∈ OP → ∅ ⊆ (Base‘𝐾))
81, 2, 3, 4, 5, 7glbval 18002 . 2 (𝐾 ∈ OP → (𝐺‘∅) = (𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥))))
9 glb0.u . . . 4 1 = (1.‘𝐾)
101, 9op1cl 37126 . . 3 (𝐾 ∈ OP → 1 ∈ (Base‘𝐾))
11 ral0 4440 . . . . . . 7 𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦
1211a1bi 362 . . . . . 6 (𝑧(le‘𝐾)𝑥 ↔ (∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥))
1312ralbii 3090 . . . . 5 (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥 ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥))
14 ral0 4440 . . . . . 6 𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦
1514biantrur 530 . . . . 5 (∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥) ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥)))
1613, 15bitri 274 . . . 4 (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥 ↔ (∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥)))
1710adantr 480 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → 1 ∈ (Base‘𝐾))
18 breq1 5073 . . . . . . . 8 (𝑧 = 1 → (𝑧(le‘𝐾)𝑥1 (le‘𝐾)𝑥))
1918rspcv 3547 . . . . . . 7 ( 1 ∈ (Base‘𝐾) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥1 (le‘𝐾)𝑥))
2017, 19syl 17 . . . . . 6 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥1 (le‘𝐾)𝑥))
211, 2, 9op1le 37133 . . . . . 6 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → ( 1 (le‘𝐾)𝑥𝑥 = 1 ))
2220, 21sylibd 238 . . . . 5 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥𝑥 = 1 ))
231, 2, 9ople1 37132 . . . . . . . . . 10 ((𝐾 ∈ OP ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧(le‘𝐾) 1 )
2423adantlr 711 . . . . . . . . 9 (((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) ∧ 𝑧 ∈ (Base‘𝐾)) → 𝑧(le‘𝐾) 1 )
2524ex 412 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → 𝑧(le‘𝐾) 1 ))
26 breq2 5074 . . . . . . . . 9 (𝑥 = 1 → (𝑧(le‘𝐾)𝑥𝑧(le‘𝐾) 1 ))
2726biimprcd 249 . . . . . . . 8 (𝑧(le‘𝐾) 1 → (𝑥 = 1𝑧(le‘𝐾)𝑥))
2825, 27syl6 35 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑧 ∈ (Base‘𝐾) → (𝑥 = 1𝑧(le‘𝐾)𝑥)))
2928com23 86 . . . . . 6 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 1 → (𝑧 ∈ (Base‘𝐾) → 𝑧(le‘𝐾)𝑥)))
3029ralrimdv 3111 . . . . 5 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (𝑥 = 1 → ∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥))
3122, 30impbid 211 . . . 4 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → (∀𝑧 ∈ (Base‘𝐾)𝑧(le‘𝐾)𝑥𝑥 = 1 ))
3216, 31bitr3id 284 . . 3 ((𝐾 ∈ OP ∧ 𝑥 ∈ (Base‘𝐾)) → ((∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥)) ↔ 𝑥 = 1 ))
3310, 32riota5 7242 . 2 (𝐾 ∈ OP → (𝑥 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑥(le‘𝐾)𝑦 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦 ∈ ∅ 𝑧(le‘𝐾)𝑦𝑧(le‘𝐾)𝑥))) = 1 )
348, 33eqtrd 2778 1 (𝐾 ∈ OP → (𝐺‘∅) = 1 )
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1539  wcel 2108  wral 3063  wss 3883  c0 4253   class class class wbr 5070  cfv 6418  crio 7211  Basecbs 16840  lecple 16895  glbcglb 17943  1.cp1 18057  OPcops 37113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-proset 17928  df-poset 17946  df-lub 17979  df-glb 17980  df-p1 18059  df-oposet 37117
This theorem is referenced by:  pmapglb2N  37712  pmapglb2xN  37713
  Copyright terms: Public domain W3C validator