Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lubeldm2d Structured version   Visualization version   GIF version

Theorem lubeldm2d 46209
Description: Member of the domain of the least upper bound function of a poset. (Contributed by Zhi Wang, 28-Sep-2024.)
Hypotheses
Ref Expression
lubeldm2d.b (𝜑𝐵 = (Base‘𝐾))
lubeldm2d.l (𝜑 = (le‘𝐾))
lubeldm2d.u (𝜑𝑈 = (lub‘𝐾))
lubeldm2d.p ((𝜑𝑥𝐵) → (𝜓 ↔ (∀𝑦𝑆 𝑦 𝑥 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑦 𝑧𝑥 𝑧))))
lubeldm2d.k (𝜑𝐾 ∈ Poset)
Assertion
Ref Expression
lubeldm2d (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆𝐵 ∧ ∃𝑥𝐵 𝜓)))
Distinct variable groups:   𝑥,𝐾,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜓(𝑥,𝑦,𝑧)   𝐵(𝑥,𝑦,𝑧)   𝑈(𝑥,𝑦,𝑧)   (𝑥,𝑦,𝑧)

Proof of Theorem lubeldm2d
StepHypRef Expression
1 eqid 2738 . . 3 (Base‘𝐾) = (Base‘𝐾)
2 eqid 2738 . . 3 (le‘𝐾) = (le‘𝐾)
3 eqid 2738 . . 3 (lub‘𝐾) = (lub‘𝐾)
4 biid 260 . . 3 ((∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))
5 lubeldm2d.k . . 3 (𝜑𝐾 ∈ Poset)
61, 2, 3, 4, 5lubeldm2 46207 . 2 (𝜑 → (𝑆 ∈ dom (lub‘𝐾) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))))
7 lubeldm2d.u . . . 4 (𝜑𝑈 = (lub‘𝐾))
87dmeqd 5809 . . 3 (𝜑 → dom 𝑈 = dom (lub‘𝐾))
98eleq2d 2824 . 2 (𝜑 → (𝑆 ∈ dom 𝑈𝑆 ∈ dom (lub‘𝐾)))
10 lubeldm2d.b . . . 4 (𝜑𝐵 = (Base‘𝐾))
1110sseq2d 3954 . . 3 (𝜑 → (𝑆𝐵𝑆 ⊆ (Base‘𝐾)))
12 lubeldm2d.p . . . . . . 7 ((𝜑𝑥𝐵) → (𝜓 ↔ (∀𝑦𝑆 𝑦 𝑥 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑦 𝑧𝑥 𝑧))))
13 lubeldm2d.l . . . . . . . . . . 11 (𝜑 = (le‘𝐾))
1413breqd 5086 . . . . . . . . . 10 (𝜑 → (𝑦 𝑥𝑦(le‘𝐾)𝑥))
1514ralbidv 3119 . . . . . . . . 9 (𝜑 → (∀𝑦𝑆 𝑦 𝑥 ↔ ∀𝑦𝑆 𝑦(le‘𝐾)𝑥))
1613breqd 5086 . . . . . . . . . . . 12 (𝜑 → (𝑦 𝑧𝑦(le‘𝐾)𝑧))
1716ralbidv 3119 . . . . . . . . . . 11 (𝜑 → (∀𝑦𝑆 𝑦 𝑧 ↔ ∀𝑦𝑆 𝑦(le‘𝐾)𝑧))
1813breqd 5086 . . . . . . . . . . 11 (𝜑 → (𝑥 𝑧𝑥(le‘𝐾)𝑧))
1917, 18imbi12d 345 . . . . . . . . . 10 (𝜑 → ((∀𝑦𝑆 𝑦 𝑧𝑥 𝑧) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))
2010, 19raleqbidv 3335 . . . . . . . . 9 (𝜑 → (∀𝑧𝐵 (∀𝑦𝑆 𝑦 𝑧𝑥 𝑧) ↔ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))
2115, 20anbi12d 631 . . . . . . . 8 (𝜑 → ((∀𝑦𝑆 𝑦 𝑥 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑦 𝑧𝑥 𝑧)) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
2221adantr 481 . . . . . . 7 ((𝜑𝑥𝐵) → ((∀𝑦𝑆 𝑦 𝑥 ∧ ∀𝑧𝐵 (∀𝑦𝑆 𝑦 𝑧𝑥 𝑧)) ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
2312, 22bitrd 278 . . . . . 6 ((𝜑𝑥𝐵) → (𝜓 ↔ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
2423pm5.32da 579 . . . . 5 (𝜑 → ((𝑥𝐵𝜓) ↔ (𝑥𝐵 ∧ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))))
2510eleq2d 2824 . . . . . 6 (𝜑 → (𝑥𝐵𝑥 ∈ (Base‘𝐾)))
2625anbi1d 630 . . . . 5 (𝜑 → ((𝑥𝐵 ∧ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))))
2724, 26bitrd 278 . . . 4 (𝜑 → ((𝑥𝐵𝜓) ↔ (𝑥 ∈ (Base‘𝐾) ∧ (∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))))
2827rexbidv2 3223 . . 3 (𝜑 → (∃𝑥𝐵 𝜓 ↔ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧))))
2911, 28anbi12d 631 . 2 (𝜑 → ((𝑆𝐵 ∧ ∃𝑥𝐵 𝜓) ↔ (𝑆 ⊆ (Base‘𝐾) ∧ ∃𝑥 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑥 ∧ ∀𝑧 ∈ (Base‘𝐾)(∀𝑦𝑆 𝑦(le‘𝐾)𝑧𝑥(le‘𝐾)𝑧)))))
306, 9, 293bitr4d 311 1 (𝜑 → (𝑆 ∈ dom 𝑈 ↔ (𝑆𝐵 ∧ ∃𝑥𝐵 𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wcel 2106  wral 3064  wrex 3065  wss 3888   class class class wbr 5075  dom cdm 5586  cfv 6428  Basecbs 16901  lecple 16958  Posetcpo 18014  lubclub 18016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5210  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-iota 6386  df-fun 6430  df-fn 6431  df-f 6432  df-f1 6433  df-fo 6434  df-f1o 6435  df-fv 6436  df-riota 7226  df-proset 18002  df-poset 18020  df-lub 18053
This theorem is referenced by:  ipolubdm  46230
  Copyright terms: Public domain W3C validator