Definition df-dmd 31397

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 <x,y> is a dual modular pair." See dmdbr 31415 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

Step	Hyp	Ref	Expression
1		cdmd 30083	. 2 class 𝑀ℋ*
2		vx	. . . . . . 7 setvar 𝑥
3	2	cv 1540	. . . . . 6 class 𝑥
4		cch 30045	. . . . . 6 class Cℋ
5	3, 4	wcel 2106	. . . . 5 wff 𝑥 ∈ Cℋ
6		vy	. . . . . . 7 setvar 𝑦
7	6	cv 1540	. . . . . 6 class 𝑦
8	7, 4	wcel 2106	. . . . 5 wff 𝑦 ∈ Cℋ
9	5, 8	wa 396	. . . 4 wff (𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ )
10		vz	. . . . . . . 8 setvar 𝑧
11	10	cv 1540	. . . . . . 7 class 𝑧
12	7, 11	wss 3944	. . . . . 6 wff 𝑦 ⊆ 𝑧
13	11, 3	cin 3943	. . . . . . . 8 class (𝑧 ∩ 𝑥)
14		chj 30049	. . . . . . . 8 class ∨ℋ
15	13, 7, 14	co 7393	. . . . . . 7 class ((𝑧 ∩ 𝑥) ∨ℋ 𝑦)
16	3, 7, 14	co 7393	. . . . . . . 8 class (𝑥 ∨ℋ 𝑦)
17	11, 16	cin 3943	. . . . . . 7 class (𝑧 ∩ (𝑥 ∨ℋ 𝑦))
18	15, 17	wceq 1541	. . . . . 6 wff ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))
19	12, 18	wi 4	. . . . 5 wff (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦)))
20	19, 10, 4	wral 3060	. . . 4 wff ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦)))
21	9, 20	wa 396	. . 3 wff ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))
22	21, 2, 6	copab 5203	. 2 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))}
23	1, 22	wceq 1541	1 wff 𝑀ℋ* = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))}

This definition is referenced by:  dmdbr  31415