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

Metamath Proof Explorer

Definition df-cmtN

Description: Define the commutes relation for orthoposets. Definition of commutes in Kalmbach p. 20. (Contributed by NM, 6-Nov-2011)

Ref Expression
Assertion df-cmtN cm = ( 𝑝 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccmtN ⊢ cm
1 vp ⊢ 𝑝
2 cvv ⊢ V
3 vx ⊢ 𝑥
4 vy ⊢ 𝑦
5 3 cv ⊢ 𝑥
6 cbs ⊢ Base
7 1 cv ⊢ 𝑝
8 7 6 cfv ⊢ ( Base ‘ 𝑝 )
9 5 8 wcel ⊢ 𝑥 ∈ ( Base ‘ 𝑝 )
10 4 cv ⊢ 𝑦
11 10 8 wcel ⊢ 𝑦 ∈ ( Base ‘ 𝑝 )
12 cmee ⊢ meet
13 7 12 cfv ⊢ ( meet ‘ 𝑝 )
14 5 10 13 co ⊢ ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 )
15 cjn ⊢ join
16 7 15 cfv ⊢ ( join ‘ 𝑝 )
17 coc ⊢ oc
18 7 17 cfv ⊢ ( oc ‘ 𝑝 )
19 10 18 cfv ⊢ ( ( oc ‘ 𝑝 ) ‘ 𝑦 )
20 5 19 13 co ⊢ ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) )
21 14 20 16 co ⊢ ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) )
22 5 21 wceq ⊢ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) )
23 9 11 22 w3a ⊢ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) )
24 23 3 4 copab ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) }
25 1 2 24 cmpt ⊢ ( 𝑝 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } )
26 0 25 wceq ⊢ cm = ( 𝑝 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } )