Definition df-md 5713

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

Assertion

Ref	Expression
df-md	|- MH = {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y))))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-md

Step	Hyp	Ref	Expression
1		cmd 4982	. 2 class MH
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cch 4968	. . . . . 6 class CH
5	3, 4	wcel 1092	. . . . 5 wff x e. CH
6		vy	. . . . . . 7 set y
7	6	cv 1089	. . . . . 6 class y
8	7, 4	wcel 1092	. . . . 5 wff y e. CH
9	5, 8	wa 196	. . . 4 wff (x e. CH /\ y e. CH)
10		vz	. . . . . . . 8 set z
11	10	cv 1089	. . . . . . 7 class z
12	11, 7	wss 1487	. . . . . 6 wff z (_ y
13		chj 4972	. . . . . . . . 9 class vH
14	11, 3, 13	co 3001	. . . . . . . 8 class (z vH x)
15	14, 7	cin 1486	. . . . . . 7 class ((z vH x) i^i y)
16	3, 7	cin 1486	. . . . . . . 8 class (x i^i y)
17	11, 16, 13	co 3001	. . . . . . 7 class (z vH (x i^i y))
18	15, 17	wceq 1091	. . . . . 6 wff ((z vH x) i^i y) = (z vH (x i^i y))
19	12, 18	wi 2	. . . . 5 wff (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y)))
20	19, 10, 4	wral 1201	. . . 4 wff A.z e. CH (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y)))
21	9, 20	wa 196	. . 3 wff ((x e. CH /\ y e. CH) /\ A.z e. CH (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y))))
22	21, 2, 6	copab 2055	. 2 class {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y))))}
23	1, 22	wceq 1091	1 wff MH = {<.x, y>. | ((x e. CH /\ y e. CH) /\ A.z e. CH (z (_ y -> ((z vH x) i^i y) = (z vH (x i^i y))))}

This definition is referenced by:  mdbr 5726

metamath.org