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

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 eqtrid ⊢ ( 𝐾 ∈ V → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } )
35 6 34 syl ⊢ ( 𝐾 ∈ 𝐴 → 𝐶 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ( ( 𝑥 ∧ 𝑦 ) ∨ ( 𝑥 ∧ ( ⊥ ‘ 𝑦 ) ) ) ) } )