MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-meet Structured version   Visualization version   GIF version

Definition df-meet 16743
Description: Define poset join. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 8-Sep-2018.)
Assertion
Ref Expression
df-meet meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Distinct variable group:   𝑥,𝑝,𝑦,𝑧

Detailed syntax breakdown of Definition df-meet
StepHypRef Expression
1 cmee 16711 . 2 class meet
2 vp . . 3 setvar 𝑝
3 cvv 3169 . . 3 class V
4 vx . . . . . . 7 setvar 𝑥
54cv 1473 . . . . . 6 class 𝑥
6 vy . . . . . . 7 setvar 𝑦
76cv 1473 . . . . . 6 class 𝑦
85, 7cpr 4123 . . . . 5 class {𝑥, 𝑦}
9 vz . . . . . 6 setvar 𝑧
109cv 1473 . . . . 5 class 𝑧
112cv 1473 . . . . . 6 class 𝑝
12 cglb 16709 . . . . . 6 class glb
1311, 12cfv 5787 . . . . 5 class (glb‘𝑝)
148, 10, 13wbr 4574 . . . 4 wff {𝑥, 𝑦} (glb‘𝑝)𝑧
1514, 4, 6, 9coprab 6525 . . 3 class {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧}
162, 3, 15cmpt 4634 . 2 class (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
171, 16wceq 1474 1 wff meet = (𝑝 ∈ V ↦ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ {𝑥, 𝑦} (glb‘𝑝)𝑧})
Colors of variables: wff setvar class
This definition is referenced by:  meetfval  16781
  Copyright terms: Public domain W3C validator