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

Definition df-dmd 29471
 Description: Define the dual 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 is a dual modular pair." See dmdbr 29489 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-dmd 𝑀* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦))))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-dmd
StepHypRef Expression
1 cdmd 28155 . 2 class 𝑀*
2 vx . . . . . . 7 setvar 𝑥
32cv 1631 . . . . . 6 class 𝑥
4 cch 28117 . . . . . 6 class C
53, 4wcel 2140 . . . . 5 wff 𝑥C
6 vy . . . . . . 7 setvar 𝑦
76cv 1631 . . . . . 6 class 𝑦
87, 4wcel 2140 . . . . 5 wff 𝑦C
95, 8wa 383 . . . 4 wff (𝑥C𝑦C )
10 vz . . . . . . . 8 setvar 𝑧
1110cv 1631 . . . . . . 7 class 𝑧
127, 11wss 3716 . . . . . 6 wff 𝑦𝑧
1311, 3cin 3715 . . . . . . . 8 class (𝑧𝑥)
14 chj 28121 . . . . . . . 8 class
1513, 7, 14co 6815 . . . . . . 7 class ((𝑧𝑥) ∨ 𝑦)
163, 7, 14co 6815 . . . . . . . 8 class (𝑥 𝑦)
1711, 16cin 3715 . . . . . . 7 class (𝑧 ∩ (𝑥 𝑦))
1815, 17wceq 1632 . . . . . 6 wff ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦))
1912, 18wi 4 . . . . 5 wff (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦)))
2019, 10, 4wral 3051 . . . 4 wff 𝑧C (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦)))
219, 20wa 383 . . 3 wff ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦))))
2221, 2, 6copab 4865 . 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦))))}
231, 22wceq 1632 1 wff 𝑀* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥C𝑦C ) ∧ ∀𝑧C (𝑦𝑧 → ((𝑧𝑥) ∨ 𝑦) = (𝑧 ∩ (𝑥 𝑦))))}
 Colors of variables: wff setvar class This definition is referenced by:  dmdbr  29489
 Copyright terms: Public domain W3C validator