Definition df-md 10145

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 mdbrt 10159 for membership relation.

Assertion

Ref	Expression
df-md	⊢ Mℋ = {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-md

Step	Hyp	Ref	Expression
1		cmd 8774	. 2 class Mℋ
2		vx	. . . . . . 7 set x
3	2	cv 953	. . . . . 6 class x
4		cch 8737	. . . . . 6 class Cℋ
5	3, 4	wcel 956	. . . . 5 wff x ∈ Cℋ
6		vy	. . . . . . 7 set y
7	6	cv 953	. . . . . 6 class y
8	7, 4	wcel 956	. . . . 5 wff y ∈ Cℋ
9	5, 8	wa 223	. . . 4 wff (x ∈ Cℋ ⋀ y ∈ Cℋ )
10		vz	. . . . . . . 8 set z
11	10	cv 953	. . . . . . 7 class z
12	11, 7	wss 2043	. . . . . 6 wff z ⊆ y
13		chj 8741	. . . . . . . . 9 class ∨ℋ
14	11, 3, 13	co 3954	. . . . . . . 8 class (z ∨ℋ x)
15	14, 7	cin 2042	. . . . . . 7 class ((z ∨ℋ x) ∩ y)
16	3, 7	cin 2042	. . . . . . . 8 class (x ∩ y)
17	11, 16, 13	co 3954	. . . . . . 7 class (z ∨ℋ (x ∩ y))
18	15, 17	wceq 954	. . . . . 6 wff ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))
19	12, 18	wi 3	. . . . 5 wff (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y)))
20	19, 10, 4	wral 1642	. . . 4 wff ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y)))
21	9, 20	wa 223	. . 3 wff ((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))))
22	21, 2, 6	copab 2661	. 2 class {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))))}
23	1, 22	wceq 954	1 wff Mℋ = {⟨x, y⟩∣((x ∈ Cℋ ⋀ y ∈ Cℋ ) ⋀ ∀z ∈ Cℋ (z ⊆ y → ((z ∨ℋ x) ∩ y) = (z ∨ℋ (x ∩ y))))}

This definition is referenced by:  mdbrt 10159

Copyright terms: Public domain