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=mVRT
mdvval.d D=mDVT
Assertion mdvval D=V×VI

Proof

Step Hyp Ref Expression
1 mdvval.v V=mVRT
2 mdvval.d D=mDVT
3 fveq2 t=TmVRt=mVRT
4 3 1 eqtr4di t=TmVRt=V
5 4 sqxpeqd t=TmVRt×mVRt=V×V
6 5 difeq1d t=TmVRt×mVRtI=V×VI
7 df-mdv mDV=tVmVRt×mVRtI
8 fvex mVRtV
9 8 8 xpex mVRt×mVRtV
10 difexg mVRt×mVRtVmVRt×mVRtIV
11 9 10 ax-mp mVRt×mVRtIV
12 6 7 11 fvmpt3i TVmDVT=V×VI
13 0dif I=
14 13 eqcomi =I
15 fvprc ¬TVmDVT=
16 fvprc ¬TVmVRT=
17 1 16 eqtrid ¬TVV=
18 17 xpeq2d ¬TVV×V=V×
19 xp0 V×=
20 18 19 eqtrdi ¬TVV×V=
21 20 difeq1d ¬TVV×VI=I
22 14 15 21 3eqtr4a ¬TVmDVT=V×VI
23 12 22 pm2.61i mDVT=V×VI
24 2 23 eqtri D=V×VI