Step | Hyp | Ref
| Expression |
1 | | vtxdeqd.v |
. . 3
⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺)) |
2 | | vtxdeqd.i |
. . . . . . 7
⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺)) |
3 | 2 | dmeqd 5811 |
. . . . . 6
⊢ (𝜑 → dom (iEdg‘𝐻) = dom (iEdg‘𝐺)) |
4 | 2 | fveq1d 6770 |
. . . . . . 7
⊢ (𝜑 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) |
5 | 4 | eleq2d 2825 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ((iEdg‘𝐻)‘𝑥) ↔ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥))) |
6 | 3, 5 | rabeqbidv 3418 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) |
7 | 6 | fveq2d 6772 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)})) |
8 | 4 | eqeq1d 2741 |
. . . . . 6
⊢ (𝜑 → (((iEdg‘𝐻)‘𝑥) = {𝑢} ↔ ((iEdg‘𝐺)‘𝑥) = {𝑢})) |
9 | 3, 8 | rabeqbidv 3418 |
. . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}}) |
10 | 9 | fveq2d 6772 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}}) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})) |
11 | 7, 10 | oveq12d 7286 |
. . 3
⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}})) = ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}}))) |
12 | 1, 11 | mpteq12dv 5169 |
. 2
⊢ (𝜑 → (𝑢 ∈ (Vtx‘𝐻) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
13 | | vtxdeqd.h |
. . 3
⊢ (𝜑 → 𝐻 ∈ 𝑌) |
14 | | eqid 2739 |
. . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
15 | | eqid 2739 |
. . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) |
16 | | eqid 2739 |
. . . 4
⊢ dom
(iEdg‘𝐻) = dom
(iEdg‘𝐻) |
17 | 14, 15, 16 | vtxdgfval 27815 |
. . 3
⊢ (𝐻 ∈ 𝑌 → (VtxDeg‘𝐻) = (𝑢 ∈ (Vtx‘𝐻) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}})))) |
18 | 13, 17 | syl 17 |
. 2
⊢ (𝜑 → (VtxDeg‘𝐻) = (𝑢 ∈ (Vtx‘𝐻) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}})))) |
19 | | vtxdeqd.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ 𝑋) |
20 | | eqid 2739 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
21 | | eqid 2739 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
22 | | eqid 2739 |
. . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
23 | 20, 21, 22 | vtxdgfval 27815 |
. . 3
⊢ (𝐺 ∈ 𝑋 → (VtxDeg‘𝐺) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
24 | 19, 23 | syl 17 |
. 2
⊢ (𝜑 → (VtxDeg‘𝐺) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}})))) |
25 | 12, 18, 24 | 3eqtr4d 2789 |
1
⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) |