Theorem mdvval

Description: The set of disjoint variable conditions, which are pairs of distinct variables. (This definition differs from appendix C, which uses unordered pairs instead. We use ordered pairs, but all sets of disjoint variable conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mdvval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mdvval.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
Assertion	mdvval	⊢ 𝐷 = ( ( 𝑉 × 𝑉 ) ∖ I )

Proof

Step	Hyp	Ref	Expression
1		mdvval.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mdvval.d	⊢ 𝐷 = ( mDV ‘ 𝑇 )
3		fveq2	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = ( mVR ‘ 𝑇 ) )
4	3 1	eqtr4di	⊢ ( 𝑡 = 𝑇 → ( mVR ‘ 𝑡 ) = 𝑉 )
5	4	sqxpeqd	⊢ ( 𝑡 = 𝑇 → ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) = ( 𝑉 × 𝑉 ) )
6	5	difeq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) = ( ( 𝑉 × 𝑉 ) ∖ I ) )
7		df-mdv	⊢ mDV = ( 𝑡 ∈ V ↦ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) )
8		fvex	⊢ ( mVR ‘ 𝑡 ) ∈ V
9	8 8	xpex	⊢ ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∈ V
10		difexg	⊢ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∈ V → ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) ∈ V )
11	9 10	ax-mp	⊢ ( ( ( mVR ‘ 𝑡 ) × ( mVR ‘ 𝑡 ) ) ∖ I ) ∈ V
12	6 7 11	fvmpt3i	⊢ ( 𝑇 ∈ V → ( mDV ‘ 𝑇 ) = ( ( 𝑉 × 𝑉 ) ∖ I ) )
13		0dif	⊢ ( ∅ ∖ I ) = ∅
14	13	eqcomi	⊢ ∅ = ( ∅ ∖ I )
15		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mDV ‘ 𝑇 ) = ∅ )
16		fvprc	⊢ ( ¬ 𝑇 ∈ V → ( mVR ‘ 𝑇 ) = ∅ )
17	1 16	syl5eq	⊢ ( ¬ 𝑇 ∈ V → 𝑉 = ∅ )
18	17	xpeq2d	⊢ ( ¬ 𝑇 ∈ V → ( 𝑉 × 𝑉 ) = ( 𝑉 × ∅ ) )
19		xp0	⊢ ( 𝑉 × ∅ ) = ∅
20	18 19	eqtrdi	⊢ ( ¬ 𝑇 ∈ V → ( 𝑉 × 𝑉 ) = ∅ )
21	20	difeq1d	⊢ ( ¬ 𝑇 ∈ V → ( ( 𝑉 × 𝑉 ) ∖ I ) = ( ∅ ∖ I ) )
22	14 15 21	3eqtr4a	⊢ ( ¬ 𝑇 ∈ V → ( mDV ‘ 𝑇 ) = ( ( 𝑉 × 𝑉 ) ∖ I ) )
23	12 22	pm2.61i	⊢ ( mDV ‘ 𝑇 ) = ( ( 𝑉 × 𝑉 ) ∖ I )
24	2 23	eqtri	⊢ 𝐷 = ( ( 𝑉 × 𝑉 ) ∖ I )