HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-md Structured version   Visualization version   GIF version

Definition df-md 28305
Description: Define the modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M for "the ordered pair <x,y> is a modular pair." See mdbr 28319 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.)
Assertion
Ref Expression
df-md 𝑀 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦))))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-md
StepHypRef Expression
1 cmd 26989 . 2 class 𝑀
2 vx . . . . . . 7 setvar 𝑥
32cv 1473 . . . . . 6 class 𝑥
4 cch 26952 . . . . . 6 class C
53, 4wcel 1938 . . . . 5 wff 𝑥C
6 vy . . . . . . 7 setvar 𝑦
76cv 1473 . . . . . 6 class 𝑦
87, 4wcel 1938 . . . . 5 wff 𝑦C
95, 8wa 382 . . . 4 wff (𝑥C𝑦C )
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1473 . . . . . . 7 class 𝑧
1211, 7wss 3444 . . . . . 6 wff 𝑧𝑦
13 chj 26956 . . . . . . . . 9 class
1411, 3, 13co 6431 . . . . . . . 8 class (𝑧 𝑥)
1514, 7cin 3443 . . . . . . 7 class ((𝑧 𝑥) ∩ 𝑦)
163, 7cin 3443 . . . . . . . 8 class (𝑥𝑦)
1711, 16, 13co 6431 . . . . . . 7 class (𝑧 (𝑥𝑦))
1815, 17wceq 1474 . . . . . 6 wff ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦))
1912, 18wi 4 . . . . 5 wff (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦)))
2019, 10, 4wral 2800 . . . 4 wff 𝑧C (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦)))
219, 20wa 382 . . 3 wff ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦))))
2221, 2, 6copab 4540 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦))))}
231, 22wceq 1474 1 wff 𝑀 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑧𝑦 → ((𝑧 𝑥) ∩ 𝑦) = (𝑧 (𝑥𝑦))))}
Colors of variables: wff setvar class
This definition is referenced by:  mdbr  28319
  Copyright terms: Public domain W3C validator