Definition df-md

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 is a modular pair." See mdbr for membership relation. (Contributed by NM, 14-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	df-md	$$⊢{𝑀}_{\mathscr{H}}=\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \forall z\in {\mathbf{C}}_{\mathscr{H}}\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmd	$$class{𝑀}_{\mathscr{H}}$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4		cch	$$class{\mathbf{C}}_{\mathscr{H}}$$
5	3 4	wcel	$$wffx\in {\mathbf{C}}_{\mathscr{H}}$$
6	2	cv	$$setvary$$
7	6 4	wcel	$$wffy\in {\mathbf{C}}_{\mathscr{H}}$$
8	5 7	wa	$$wff\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)$$
9		vz	$$setvarz$$
10	9	cv	$$setvarz$$
11	10 6	wss	$$wffz\subseteq y$$
12		chj	$$class{\vee }_{\mathscr{H}}$$
13	10 3 12	co	$$class\left(z{\vee }_{\mathscr{H}}x\right)$$
14	13 6	cin	$$class\left(\left(z{\vee }_{\mathscr{H}}x\right)\cap y\right)$$
15	3 6	cin	$$class\left(x\cap y\right)$$
16	10 15 12	co	$$class\left(z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)$$
17	14 16	wceq	$$wff\left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)$$
18	11 17	wi	$$wff\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)$$
19	18 9 4	wral	$$wff\forall z\in {\mathbf{C}}_{\mathscr{H}}\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)$$
20	8 19	wa	$$wff\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \forall z\in {\mathbf{C}}_{\mathscr{H}}\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)\right)$$
21	20 1 2	copab	$$class\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \forall z\in {\mathbf{C}}_{\mathscr{H}}\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)\right)\right\}$$
22	0 21	wceq	$$wff{𝑀}_{\mathscr{H}}=\left\{⟨x,y⟩|\left(\left(x\in {\mathbf{C}}_{\mathscr{H}}\wedge y\in {\mathbf{C}}_{\mathscr{H}}\right)\wedge \forall z\in {\mathbf{C}}_{\mathscr{H}}\left(z\subseteq y\to \left(z{\vee }_{\mathscr{H}}x\right)\cap y=z{\vee }_{\mathscr{H}}\left(x\cap y\right)\right)\right)\right\}$$