Step | Hyp | Ref
| Expression |
1 | | df-vdgr 26421 |
. . 3
⊢ VDeg =
(𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})))) |
2 | 1 | a1i 11 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → VDeg = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))))) |
3 | | simprl 790 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → 𝑣 = 𝑉) |
4 | | simprr 792 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → 𝑒 = 𝐸) |
5 | 4 | dmeqd 5248 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝑒 = dom 𝐸) |
6 | | simpl2 1058 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → 𝐸 Fn 𝐴) |
7 | | fndm 5904 |
. . . . . . . 8
⊢ (𝐸 Fn 𝐴 → dom 𝐸 = 𝐴) |
8 | 6, 7 | syl 17 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝐸 = 𝐴) |
9 | 5, 8 | eqtrd 2644 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → dom 𝑒 = 𝐴) |
10 | 4 | fveq1d 6105 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑒‘𝑥) = (𝐸‘𝑥)) |
11 | 10 | eleq2d 2673 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑢 ∈ (𝑒‘𝑥) ↔ 𝑢 ∈ (𝐸‘𝑥))) |
12 | 9, 11 | rabeqbidv 3168 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → {𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) |
13 | 12 | fveq2d 6107 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) = (#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)})) |
14 | 10 | eqeq1d 2612 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → ((𝑒‘𝑥) = {𝑢} ↔ (𝐸‘𝑥) = {𝑢})) |
15 | 9, 14 | rabeqbidv 3168 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → {𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}} = {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}) |
16 | 15 | fveq2d 6107 |
. . . 4
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}) = (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})) |
17 | 13, 16 | oveq12d 6567 |
. . 3
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) |
18 | 3, 17 | mpteq12dv 4663 |
. 2
⊢ (((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ (𝑣 = 𝑉 ∧ 𝑒 = 𝐸)) → (𝑢 ∈ 𝑣 ↦ ((#‘{𝑥 ∈ dom 𝑒 ∣ 𝑢 ∈ (𝑒‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝑒 ∣ (𝑒‘𝑥) = {𝑢}}))) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})))) |
19 | | elex 3185 |
. . 3
⊢ (𝑉 ∈ 𝑊 → 𝑉 ∈ V) |
20 | 19 | 3ad2ant1 1075 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → 𝑉 ∈ V) |
21 | | fnex 6386 |
. . 3
⊢ ((𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → 𝐸 ∈ V) |
22 | 21 | 3adant1 1072 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → 𝐸 ∈ V) |
23 | | mptexg 6389 |
. . 3
⊢ (𝑉 ∈ 𝑊 → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) ∈ V) |
24 | 23 | 3ad2ant1 1075 |
. 2
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}}))) ∈ V) |
25 | 2, 18, 20, 22, 24 | ovmpt2d 6686 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) → (𝑉 VDeg 𝐸) = (𝑢 ∈ 𝑉 ↦ ((#‘{𝑥 ∈ 𝐴 ∣ 𝑢 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑢}})))) |