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