| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vtxdeqd.v | . . 3
⊢ (𝜑 → (Vtx‘𝐻) = (Vtx‘𝐺)) | 
| 2 |  | vtxdeqd.i | . . . . . . 7
⊢ (𝜑 → (iEdg‘𝐻) = (iEdg‘𝐺)) | 
| 3 | 2 | dmeqd 5915 | . . . . . 6
⊢ (𝜑 → dom (iEdg‘𝐻) = dom (iEdg‘𝐺)) | 
| 4 | 2 | fveq1d 6907 | . . . . . . 7
⊢ (𝜑 → ((iEdg‘𝐻)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) | 
| 5 | 4 | eleq2d 2826 | . . . . . 6
⊢ (𝜑 → (𝑢 ∈ ((iEdg‘𝐻)‘𝑥) ↔ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥))) | 
| 6 | 3, 5 | rabeqbidv 3454 | . . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) | 
| 7 | 6 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)})) | 
| 8 | 4 | eqeq1d 2738 | . . . . . 6
⊢ (𝜑 → (((iEdg‘𝐻)‘𝑥) = {𝑢} ↔ ((iEdg‘𝐺)‘𝑥) = {𝑢})) | 
| 9 | 3, 8 | rabeqbidv 3454 | . . . . 5
⊢ (𝜑 → {𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}} = {𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}}) | 
| 10 | 9 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ ((iEdg‘𝐻)‘𝑥) = {𝑢}}) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ ((iEdg‘𝐺)‘𝑥) = {𝑢}})) | 
| 11 | 7, 10 | oveq12d 7450 | . . 3
⊢ (𝜑 → ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}})) = ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}}))) | 
| 12 | 1, 11 | mpteq12dv 5232 | . 2
⊢ (𝜑 → (𝑢 ∈ (Vtx‘𝐻) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐻) ∣ 𝑢 ∈ ((iEdg‘𝐻)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐻) ∣
((iEdg‘𝐻)‘𝑥) = {𝑢}}))) = (𝑢 ∈ (Vtx‘𝐺) ↦ ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑢 ∈ ((iEdg‘𝐺)‘𝑥)}) +𝑒
(♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
((iEdg‘𝐺)‘𝑥) = {𝑢}})))) | 
| 13 |  | vtxdeqd.h | . . 3
⊢ (𝜑 → 𝐻 ∈ 𝑌) | 
| 14 |  | eqid 2736 | . . . 4
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) | 
| 15 |  | eqid 2736 | . . . 4
⊢
(iEdg‘𝐻) =
(iEdg‘𝐻) | 
| 16 |  | eqid 2736 | . . . 4
⊢ dom
(iEdg‘𝐻) = dom
(iEdg‘𝐻) | 
| 17 | 14, 15, 16 | vtxdgfval 29486 | . . 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 2736 | . . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 21 |  | eqid 2736 | . . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 22 |  | eqid 2736 | . . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) | 
| 23 | 20, 21, 22 | vtxdgfval 29486 | . . 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 2786 | 1
⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺)) |