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 33192
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 6726 . . . . . . 7 (𝑡 = 𝑇 → (mVR‘𝑡) = (mVR‘𝑇))
3 mdvval.v . . . . . . 7 𝑉 = (mVR‘𝑇)
42, 3eqtr4di 2797 . . . . . 6 (𝑡 = 𝑇 → (mVR‘𝑡) = 𝑉)
54sqxpeqd 5592 . . . . 5 (𝑡 = 𝑇 → ((mVR‘𝑡) × (mVR‘𝑡)) = (𝑉 × 𝑉))
65difeq1d 4045 . . . 4 (𝑡 = 𝑇 → (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) = ((𝑉 × 𝑉) ∖ I ))
7 df-mdv 33176 . . . 4 mDV = (𝑡 ∈ V ↦ (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ))
8 fvex 6739 . . . . . 6 (mVR‘𝑡) ∈ V
98, 8xpex 7547 . . . . 5 ((mVR‘𝑡) × (mVR‘𝑡)) ∈ V
10 difexg 5229 . . . . 5 (((mVR‘𝑡) × (mVR‘𝑡)) ∈ V → (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) ∈ V)
119, 10ax-mp 5 . . . 4 (((mVR‘𝑡) × (mVR‘𝑡)) ∖ I ) ∈ V
126, 7, 11fvmpt3i 6832 . . 3 (𝑇 ∈ V → (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I ))
13 0dif 4325 . . . . 5 (∅ ∖ I ) = ∅
1413eqcomi 2747 . . . 4 ∅ = (∅ ∖ I )
15 fvprc 6718 . . . 4 𝑇 ∈ V → (mDV‘𝑇) = ∅)
16 fvprc 6718 . . . . . . . 8 𝑇 ∈ V → (mVR‘𝑇) = ∅)
173, 16syl5eq 2791 . . . . . . 7 𝑇 ∈ V → 𝑉 = ∅)
1817xpeq2d 5590 . . . . . 6 𝑇 ∈ V → (𝑉 × 𝑉) = (𝑉 × ∅))
19 xp0 6030 . . . . . 6 (𝑉 × ∅) = ∅
2018, 19eqtrdi 2795 . . . . 5 𝑇 ∈ V → (𝑉 × 𝑉) = ∅)
2120difeq1d 4045 . . . 4 𝑇 ∈ V → ((𝑉 × 𝑉) ∖ I ) = (∅ ∖ I ))
2214, 15, 213eqtr4a 2805 . . 3 𝑇 ∈ V → (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I ))
2312, 22pm2.61i 185 . 2 (mDV‘𝑇) = ((𝑉 × 𝑉) ∖ I )
241, 23eqtri 2766 1 𝐷 = ((𝑉 × 𝑉) ∖ I )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1543  wcel 2111  Vcvv 3415  cdif 3872  c0 4246   I cid 5463   × cxp 5558  cfv 6389  mVRcmvar 33149  mDVcmdv 33156
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3417  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4829  df-br 5063  df-opab 5125  df-mpt 5145  df-id 5464  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-iota 6347  df-fun 6391  df-fv 6397  df-mdv 33176
This theorem is referenced by:  mthmpps  33270  mclsppslem  33271
  Copyright terms: Public domain W3C validator