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

Definition df-mvl 33294
Description: Define the set of valuations. (Contributed by Mario Carneiro, 14-Jul-2016.)
Assertion
Ref Expression
df-mvl mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)}))
Distinct variable group:   𝑣,𝑡

Detailed syntax breakdown of Definition df-mvl
StepHypRef Expression
1 cmvl 33281 . 2 class mVL
2 vt . . 3 setvar 𝑡
3 cvv 3408 . . 3 class V
4 vv . . . 4 setvar 𝑣
52cv 1542 . . . . 5 class 𝑡
6 cmvar 33136 . . . . 5 class mVR
75, 6cfv 6380 . . . 4 class (mVR‘𝑡)
8 cmuv 33280 . . . . . 6 class mUV
95, 8cfv 6380 . . . . 5 class (mUV‘𝑡)
104cv 1542 . . . . . . 7 class 𝑣
11 cmty 33137 . . . . . . . 8 class mType
125, 11cfv 6380 . . . . . . 7 class (mType‘𝑡)
1310, 12cfv 6380 . . . . . 6 class ((mType‘𝑡)‘𝑣)
1413csn 4541 . . . . 5 class {((mType‘𝑡)‘𝑣)}
159, 14cima 5554 . . . 4 class ((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})
164, 7, 15cixp 8578 . . 3 class X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)})
172, 3, 16cmpt 5135 . 2 class (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)}))
181, 17wceq 1543 1 wff mVL = (𝑡 ∈ V ↦ X𝑣 ∈ (mVR‘𝑡)((mUV‘𝑡) “ {((mType‘𝑡)‘𝑣)}))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator