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	$⊢ 𝑀_{ℋ}^{*} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y)))\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmd	$class 𝑀_{ℋ}^{*}$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		cch	$class C_{ℋ}$
5	3 4	wcel	$wff x \in C_{ℋ}$
6	2	cv	$setvar y$
7	6 4	wcel	$wff y \in C_{ℋ}$
8	5 7	wa	$wff (x \in C_{ℋ} \land y \in C_{ℋ})$
9		vz	$setvar z$
10	9	cv	$setvar z$
11	6 10	wss	$wff y \subseteq z$
12	10 3	cin	$class (z \cap x)$
13		chj	$class \lor_{ℋ}$
14	12 6 13	co	$class ((z \cap x) \lor_{ℋ} y)$
15	3 6 13	co	$class (x \lor_{ℋ} y)$
16	10 15	cin	$class (z \cap (x \lor_{ℋ} y))$
17	14 16	wceq	$wff (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y)$
18	11 17	wi	$wff (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y))$
19	18 9 4	wral	$wff \forall z \in C_{ℋ} (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y))$
20	8 19	wa	$wff ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y)))$
21	20 1 2	copab	$class \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y)))\}$
22	0 21	wceq	$wff 𝑀_{ℋ}^{*} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (y \subseteq z \to (z \cap x) \lor_{ℋ} y = z \cap (x \lor_{ℋ} y)))\}$

Metamath Proof Explorer

Definition df-dmd

Detailed syntax breakdown