| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 2 | | 1egrvtxdg1.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
| 3 | | 1egrvtxdg1.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
| 4 | | 1egrvtxdg1.v |
. . . . 5
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) |
| 5 | 3, 4 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (Vtx‘𝐺)) |
| 6 | | 1egrvtxdg1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
| 7 | 6, 4 | eleqtrrd 2844 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (Vtx‘𝐺)) |
| 8 | | 1egrvtxdg1.i |
. . . 4
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) |
| 9 | | 1egrvtxdg1.n |
. . . 4
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
| 10 | 1, 2, 5, 7, 8, 9 | usgr1e 29262 |
. . 3
⊢ (𝜑 → 𝐺 ∈ USGraph) |
| 11 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 12 | | eqid 2737 |
. . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
| 13 | | eqid 2737 |
. . . 4
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
| 14 | 1, 11, 12, 13 | vtxdusgrval 29505 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐵 ∈ (Vtx‘𝐺)) → ((VtxDeg‘𝐺)‘𝐵) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)})) |
| 15 | 10, 5, 14 | syl2anc 584 |
. 2
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)})) |
| 16 | | dmeq 5914 |
. . . . . . . 8
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → dom (iEdg‘𝐺) = dom {〈𝐴, {𝐵, 𝐶}〉}) |
| 17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom (iEdg‘𝐺) = dom {〈𝐴, {𝐵, 𝐶}〉}) |
| 18 | | prex 5437 |
. . . . . . . 8
⊢ {𝐵, 𝐶} ∈ V |
| 19 | | dmsnopg 6233 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ V → dom {〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
| 20 | 18, 19 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom {〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
| 21 | 17, 20 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom (iEdg‘𝐺) = {𝐴}) |
| 22 | | fveq1 6905 |
. . . . . . . 8
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → ((iEdg‘𝐺)‘𝑥) = ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)) |
| 23 | 22 | eleq2d 2827 |
. . . . . . 7
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → (𝐵 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥))) |
| 24 | 23 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (𝐵 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥))) |
| 25 | 21, 24 | rabeqbidv 3455 |
. . . . 5
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) |
| 26 | 25 | fveq2d 6910 |
. . . 4
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)})) |
| 27 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥) = ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴)) |
| 28 | 27 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴))) |
| 29 | 28 | rabsnif 4723 |
. . . . . . . 8
⊢ {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)} = if(𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴), {𝐴}, ∅) |
| 30 | | prid1g 4760 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐶}) |
| 31 | 3, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵, 𝐶}) |
| 32 | | fvsng 7200 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ {𝐵, 𝐶} ∈ V) → ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴) = {𝐵, 𝐶}) |
| 33 | 2, 18, 32 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴) = {𝐵, 𝐶}) |
| 34 | 31, 33 | eleqtrrd 2844 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴)) |
| 35 | 34 | iftrued 4533 |
. . . . . . . 8
⊢ (𝜑 → if(𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴), {𝐴}, ∅) = {𝐴}) |
| 36 | 29, 35 | eqtrid 2789 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)} = {𝐴}) |
| 37 | 36 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = (♯‘{𝐴})) |
| 38 | | hashsng 14408 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (♯‘{𝐴}) = 1) |
| 39 | 2, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝐴}) = 1) |
| 40 | 37, 39 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = 1) |
| 41 | 40 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = 1) |
| 42 | 26, 41 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
| 43 | 8, 42 | mpdan 687 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
| 44 | 15, 43 | eqtrd 2777 |
1
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) |