Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mdvval Structured version   Unicode version

Theorem mdvval 28842
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 DV conditions of interest will be symmetric, so it does not matter.) (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mdvval.v  |-  V  =  (mVR `  T )
mdvval.d  |-  D  =  (mDV `  T )
Assertion
Ref Expression
mdvval  |-  D  =  ( ( V  X.  V )  \  _I  )

Proof of Theorem mdvval
Dummy variable  t is distinct from all other variables.
StepHypRef Expression
1 mdvval.d . 2  |-  D  =  (mDV `  T )
2 fveq2 5856 . . . . . . 7  |-  ( t  =  T  ->  (mVR `  t )  =  (mVR
`  T ) )
3 mdvval.v . . . . . . 7  |-  V  =  (mVR `  T )
42, 3syl6eqr 2502 . . . . . 6  |-  ( t  =  T  ->  (mVR `  t )  =  V )
54sqxpeqd 5015 . . . . 5  |-  ( t  =  T  ->  (
(mVR `  t )  X.  (mVR `  t )
)  =  ( V  X.  V ) )
65difeq1d 3606 . . . 4  |-  ( t  =  T  ->  (
( (mVR `  t
)  X.  (mVR `  t ) )  \  _I  )  =  (
( V  X.  V
)  \  _I  )
)
7 df-mdv 28826 . . . 4  |- mDV  =  ( t  e.  _V  |->  ( ( (mVR `  t
)  X.  (mVR `  t ) )  \  _I  ) )
8 fvex 5866 . . . . . 6  |-  (mVR `  t )  e.  _V
98, 8xpex 6589 . . . . 5  |-  ( (mVR
`  t )  X.  (mVR `  t )
)  e.  _V
10 difexg 4585 . . . . 5  |-  ( ( (mVR `  t )  X.  (mVR `  t )
)  e.  _V  ->  ( ( (mVR `  t
)  X.  (mVR `  t ) )  \  _I  )  e.  _V )
119, 10ax-mp 5 . . . 4  |-  ( ( (mVR `  t )  X.  (mVR `  t )
)  \  _I  )  e.  _V
126, 7, 11fvmpt3i 5945 . . 3  |-  ( T  e.  _V  ->  (mDV `  T )  =  ( ( V  X.  V
)  \  _I  )
)
13 0dif 3885 . . . . 5  |-  ( (/)  \  _I  )  =  (/)
1413eqcomi 2456 . . . 4  |-  (/)  =  (
(/)  \  _I  )
15 fvprc 5850 . . . 4  |-  ( -.  T  e.  _V  ->  (mDV
`  T )  =  (/) )
16 fvprc 5850 . . . . . . . 8  |-  ( -.  T  e.  _V  ->  (mVR
`  T )  =  (/) )
173, 16syl5eq 2496 . . . . . . 7  |-  ( -.  T  e.  _V  ->  V  =  (/) )
1817xpeq2d 5013 . . . . . 6  |-  ( -.  T  e.  _V  ->  ( V  X.  V )  =  ( V  X.  (/) ) )
19 xp0 5415 . . . . . 6  |-  ( V  X.  (/) )  =  (/)
2018, 19syl6eq 2500 . . . . 5  |-  ( -.  T  e.  _V  ->  ( V  X.  V )  =  (/) )
2120difeq1d 3606 . . . 4  |-  ( -.  T  e.  _V  ->  ( ( V  X.  V
)  \  _I  )  =  ( (/)  \  _I  ) )
2214, 15, 213eqtr4a 2510 . . 3  |-  ( -.  T  e.  _V  ->  (mDV
`  T )  =  ( ( V  X.  V )  \  _I  ) )
2312, 22pm2.61i 164 . 2  |-  (mDV `  T )  =  ( ( V  X.  V
)  \  _I  )
241, 23eqtri 2472 1  |-  D  =  ( ( V  X.  V )  \  _I  )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1383    e. wcel 1804   _Vcvv 3095    \ cdif 3458   (/)c0 3770    _I cid 4780    X. cxp 4987   ` cfv 5578  mVRcmvar 28799  mDVcmdv 28806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-mdv 28826
This theorem is referenced by:  mthmpps  28920  mclsppslem  28921
  Copyright terms: Public domain W3C validator