Metamath Proof Explorer


Theorem cmtfvalN

Description: Value of commutes relation. (Contributed by NM, 6-Nov-2011) (New usage is discouraged.)

Ref Expression
Hypotheses cmtfval.b 𝐵 = ( Base ‘ 𝐾 )
cmtfval.j = ( join ‘ 𝐾 )
cmtfval.m = ( meet ‘ 𝐾 )
cmtfval.o = ( oc ‘ 𝐾 )
cmtfval.c 𝐶 = ( cm ‘ 𝐾 )
Assertion cmtfvalN ( 𝐾𝐴𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 cmtfval.b 𝐵 = ( Base ‘ 𝐾 )
2 cmtfval.j = ( join ‘ 𝐾 )
3 cmtfval.m = ( meet ‘ 𝐾 )
4 cmtfval.o = ( oc ‘ 𝐾 )
5 cmtfval.c 𝐶 = ( cm ‘ 𝐾 )
6 elex ( 𝐾𝐴𝐾 ∈ V )
7 fveq2 ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = ( Base ‘ 𝐾 ) )
8 7 1 eqtr4di ( 𝑝 = 𝐾 → ( Base ‘ 𝑝 ) = 𝐵 )
9 8 eleq2d ( 𝑝 = 𝐾 → ( 𝑥 ∈ ( Base ‘ 𝑝 ) ↔ 𝑥𝐵 ) )
10 8 eleq2d ( 𝑝 = 𝐾 → ( 𝑦 ∈ ( Base ‘ 𝑝 ) ↔ 𝑦𝐵 ) )
11 fveq2 ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = ( join ‘ 𝐾 ) )
12 11 2 eqtr4di ( 𝑝 = 𝐾 → ( join ‘ 𝑝 ) = )
13 fveq2 ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = ( meet ‘ 𝐾 ) )
14 13 3 eqtr4di ( 𝑝 = 𝐾 → ( meet ‘ 𝑝 ) = )
15 14 oveqd ( 𝑝 = 𝐾 → ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) = ( 𝑥 𝑦 ) )
16 eqidd ( 𝑝 = 𝐾𝑥 = 𝑥 )
17 fveq2 ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = ( oc ‘ 𝐾 ) )
18 17 4 eqtr4di ( 𝑝 = 𝐾 → ( oc ‘ 𝑝 ) = )
19 18 fveq1d ( 𝑝 = 𝐾 → ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) = ( 𝑦 ) )
20 14 16 19 oveq123d ( 𝑝 = 𝐾 → ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) = ( 𝑥 ( 𝑦 ) ) )
21 12 15 20 oveq123d ( 𝑝 = 𝐾 → ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) )
22 21 eqeq2d ( 𝑝 = 𝐾 → ( 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ↔ 𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) )
23 9 10 22 3anbi123d ( 𝑝 = 𝐾 → ( ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) ↔ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) ) )
24 23 opabbidv ( 𝑝 = 𝐾 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } )
25 df-cmtN cm = ( 𝑝 ∈ V ↦ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( Base ‘ 𝑝 ) ∧ 𝑦 ∈ ( Base ‘ 𝑝 ) ∧ 𝑥 = ( ( 𝑥 ( meet ‘ 𝑝 ) 𝑦 ) ( join ‘ 𝑝 ) ( 𝑥 ( meet ‘ 𝑝 ) ( ( oc ‘ 𝑝 ) ‘ 𝑦 ) ) ) ) } )
26 df-3an ( ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) ↔ ( ( 𝑥𝐵𝑦𝐵 ) ∧ 𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) )
27 26 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ 𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) }
28 1 fvexi 𝐵 ∈ V
29 28 28 xpex ( 𝐵 × 𝐵 ) ∈ V
30 opabssxp { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ 𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } ⊆ ( 𝐵 × 𝐵 )
31 29 30 ssexi { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ 𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } ∈ V
32 27 31 eqeltri { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } ∈ V
33 24 25 32 fvmpt ( 𝐾 ∈ V → ( cm ‘ 𝐾 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } )
34 5 33 syl5eq ( 𝐾 ∈ V → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } )
35 6 34 syl ( 𝐾𝐴𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐵𝑦𝐵𝑥 = ( ( 𝑥 𝑦 ) ( 𝑥 ( 𝑦 ) ) ) ) } )