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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmd	$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	10 6	wss	$wff z \subseteq y$
12		chj	$class \lor_{ℋ}$
13	10 3 12	co	$class (z \lor_{ℋ} x)$
14	13 6	cin	$class ((z \lor_{ℋ} x) \cap y)$
15	3 6	cin	$class (x \cap y)$
16	10 15 12	co	$class (z \lor_{ℋ} (x \cap y))$
17	14 16	wceq	$wff (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y)$
18	11 17	wi	$wff (z \subseteq y \to (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y))$
19	18 9 4	wral	$wff \forall z \in C_{ℋ} (z \subseteq y \to (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y))$
20	8 19	wa	$wff ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (z \subseteq y \to (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y)))$
21	20 1 2	copab	$class \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (z \subseteq y \to (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y)))\}$
22	0 21	wceq	$wff 𝑀_{ℋ} = \{⟨x, y⟩ \| ((x \in C_{ℋ} \land y \in C_{ℋ}) \land \forall z \in C_{ℋ} (z \subseteq y \to (z \lor_{ℋ} x) \cap y = z \lor_{ℋ} (x \cap y)))\}$

Metamath Proof Explorer

Definition df-md

Detailed syntax breakdown