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

Theorem mdvval 35867
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.)
Hypotheses
Ref Expression
mdvval.v 𝑉 = (mVR‘𝑇)
mdvval.d 𝐷 = (mDV‘𝑇)
Assertion
Ref Expression
mdvval 𝐷 = ((𝑉 × 𝑉) ∖ I )

Proof of Theorem mdvval
Dummy variable 𝑡 is distinct from all other variables.
StepHypRef Expression
1 mdvval.d . 2 𝐷 = (mDV‘𝑇)
2 fveq2 6871 . . . . . . 7 (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
3 mdvval.v . . . . . . 7 𝑉 = (mVR‘𝑇)
42, 3eqtr4di 2818 . . . . . 6 (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
54sqxpeqd 5684 . . . . 5 (𝑡 = 𝑇 → ((mVR‘𝑡) × (mVR‘𝑡)) = (𝑉 × 𝑉))
65difeq1d 4082 . . . 4 (𝑡 = 𝑇 → (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) = ((𝑉 × 𝑉) ∖ I ))
7 df-mdv 35851 . . . 4 mDV = (𝑡 ∈ V ↦ (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ))
8 fvex 6884 . . . . . 6 (mVR‘𝑡) ∈ V
98, 8xpex 7740 . . . . 5 ((mVR‘𝑡) × (mVR‘𝑡)) ∈ V
10 difexg 5290 . . . . 5 (((mVR‘𝑡) × (mVR‘𝑡)) ∈ V → (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) ∈ V)
119, 10ax-mp 5 . . . 4 (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) ∈ V
126, 7, 11fvmpt3i 6985 . . 3 (𝑇 ∈ V → (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I ))
13 0dif 4362 . . . . 5 (∅ ∖ I ) = ∅
1413eqcomi 2774 . . . 4 ∅ = (∅ ∖ I )
15 fvprc 6863 . . . 4 𝑇 ∈ V → (mDV‘𝑇) = ∅)
16 fvprc 6863 . . . . . . . 8 𝑇 ∈ V → (mVR‘𝑇) = ∅)
173, 16eqtrid 2812 . . . . . . 7 𝑇 ∈ V → 𝑉 = ∅)
1817xpeq2d 5682 . . . . . 6 𝑇 ∈ V → (𝑉 × 𝑉) = (𝑉 × ∅))
19 xp0 5752 . . . . . 6 (𝑉 × ∅) = ∅
2018, 19eqtrdi 2816 . . . . 5 𝑇 ∈ V → (𝑉 × 𝑉) = ∅)
2120difeq1d 4082 . . . 4 𝑇 ∈ V → ((𝑉 × 𝑉) ∖ I ) = (∅ ∖ I ))
2214, 15, 213eqtr4a 2826 . . 3 𝑇 ∈ V → (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I ))
2312, 22pm2.61i 184 . 2 (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I )
241, 23eqtri 2788 1 𝐷 = ((𝑉 × 𝑉) ∖ I )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1563  wcel 2145  Vcvv 3457  cdif 3904  c0 4288   I cid 5546   × cxp 5650  cfv 6525  mVRcmvar 35824  mDVcmdv 35831
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-mdv 35851
This theorem is referenced by:  mthmpps  35945  mclsppslem  35946
  Copyright terms: Public domain W3C validator