This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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ℋ ( 𝑦 ⊆ 𝑧 → ( ( 𝑧 ∩ 𝑥 ) ∨ℋ 𝑦 ) = ( 𝑧 ∩ ( 𝑥 ∨ℋ 𝑦 ) ) ) ) }