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	⊢ 𝑀ℋ* = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀ 𝑧 ∈ Cℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdmd	⊢ 𝑀ℋ*
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cch	⊢ Cℋ
5	3 4	wcel	⊢ 𝑥 ∈ Cℋ
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ Cℋ
8	5 7	wa	⊢ ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ )
9		vz	⊢ 𝑧
10	9	cv	⊢ 𝑧
11	6 10	wss	⊢ 𝑦 ⊆ 𝑧
12	10 3	cin	⊢ ( 𝑧 ∩ 𝑥 )
13		chj	⊢ ∨ℋ
14	12 6 13	co	⊢ ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 )
15	3 6 13	co	⊢ ( 𝑥 ∨ℋ 𝑦 )
16	10 15	cin	⊢ ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) )
17	14 16	wceq	⊢ ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) )
18	11 17	wi	⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) )
19	18 9 4	wral	⊢ ∀ 𝑧 ∈ Cℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) )
20	8 19	wa	⊢ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀ 𝑧 ∈ Cℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) ) )
21	20 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀ 𝑧 ∈ Cℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) ) ) }
22	0 21	wceq	⊢ 𝑀ℋ* = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀ 𝑧 ∈ Cℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) ) ) }