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 ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } )