Metamath Proof Explorer


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
|- V = ( mVR ` T )
mdvval.d
|- D = ( mDV ` T )
Assertion mdvval
|- D = ( ( V X. V ) \ _I )

Proof

Step Hyp Ref Expression
1 mdvval.v
 |-  V = ( mVR ` T )
2 mdvval.d
 |-  D = ( mDV ` T )
3 fveq2
 |-  ( t = T -> ( mVR ` t ) = ( mVR ` T ) )
4 3 1 eqtr4di
 |-  ( t = T -> ( mVR ` t ) = V )
5 4 sqxpeqd
 |-  ( t = T -> ( ( mVR ` t ) X. ( mVR ` t ) ) = ( V X. V ) )
6 5 difeq1d
 |-  ( t = T -> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) = ( ( V X. V ) \ _I ) )
7 df-mdv
 |-  mDV = ( t e. _V |-> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) )
8 fvex
 |-  ( mVR ` t ) e. _V
9 8 8 xpex
 |-  ( ( mVR ` t ) X. ( mVR ` t ) ) e. _V
10 difexg
 |-  ( ( ( mVR ` t ) X. ( mVR ` t ) ) e. _V -> ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) e. _V )
11 9 10 ax-mp
 |-  ( ( ( mVR ` t ) X. ( mVR ` t ) ) \ _I ) e. _V
12 6 7 11 fvmpt3i
 |-  ( T e. _V -> ( mDV ` T ) = ( ( V X. V ) \ _I ) )
13 0dif
 |-  ( (/) \ _I ) = (/)
14 13 eqcomi
 |-  (/) = ( (/) \ _I )
15 fvprc
 |-  ( -. T e. _V -> ( mDV ` T ) = (/) )
16 fvprc
 |-  ( -. T e. _V -> ( mVR ` T ) = (/) )
17 1 16 syl5eq
 |-  ( -. T e. _V -> V = (/) )
18 17 xpeq2d
 |-  ( -. T e. _V -> ( V X. V ) = ( V X. (/) ) )
19 xp0
 |-  ( V X. (/) ) = (/)
20 18 19 eqtrdi
 |-  ( -. T e. _V -> ( V X. V ) = (/) )
21 20 difeq1d
 |-  ( -. T e. _V -> ( ( V X. V ) \ _I ) = ( (/) \ _I ) )
22 14 15 21 3eqtr4a
 |-  ( -. T e. _V -> ( mDV ` T ) = ( ( V X. V ) \ _I ) )
23 12 22 pm2.61i
 |-  ( mDV ` T ) = ( ( V X. V ) \ _I )
24 2 23 eqtri
 |-  D = ( ( V X. V ) \ _I )