Definition df-dmd

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 for membership relation. (Contributed by NM, 27-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	df-dmd	$$⊢{𝑀}_{\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(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}y\right)\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmd	$$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	6 10	wss	$$wffy\subseteq z$$
12	10 3	cin	$$class\left(z\cap x\right)$$
13		chj	$$class{\vee }_{\mathscr{H}}$$
14	12 6 13	co	$$class\left(\left(z\cap x\right){\vee }_{\mathscr{H}}y\right)$$
15	3 6 13	co	$$class\left(x{\vee }_{\mathscr{H}}y\right)$$
16	10 15	cin	$$class\left(z\cap \left(x{\vee }_{\mathscr{H}}y\right)\right)$$
17	14 16	wceq	$$wff\left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}y\right)$$
18	11 17	wi	$$wff\left(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}y\right)\right)$$
19	18 9 4	wral	$$wff\forall z\in {\mathbf{C}}_{\mathscr{H}}\left(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}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(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}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(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}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(y\subseteq z\to \left(z\cap x\right){\vee }_{\mathscr{H}}y=z\cap \left(x{\vee }_{\mathscr{H}}y\right)\right)\right)\right\}$$