Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | 1egrvtxdg1.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
3 | | 1egrvtxdg1.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
4 | | 1egrvtxdg1.v |
. . . . 5
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) |
5 | 3, 4 | eleqtrrd 2842 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ (Vtx‘𝐺)) |
6 | | 1egrvtxdg1.c |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
7 | 6, 4 | eleqtrrd 2842 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (Vtx‘𝐺)) |
8 | | 1egrvtxdg1.i |
. . . 4
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) |
9 | | 1egrvtxdg1.n |
. . . 4
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
10 | 1, 2, 5, 7, 8, 9 | usgr1e 27612 |
. . 3
⊢ (𝜑 → 𝐺 ∈ USGraph) |
11 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
12 | | eqid 2738 |
. . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
13 | | eqid 2738 |
. . . 4
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
14 | 1, 11, 12, 13 | vtxdusgrval 27854 |
. . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝐵 ∈ (Vtx‘𝐺)) → ((VtxDeg‘𝐺)‘𝐵) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)})) |
15 | 10, 5, 14 | syl2anc 584 |
. 2
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)})) |
16 | | dmeq 5812 |
. . . . . . . 8
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → dom (iEdg‘𝐺) = dom {〈𝐴, {𝐵, 𝐶}〉}) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom (iEdg‘𝐺) = dom {〈𝐴, {𝐵, 𝐶}〉}) |
18 | | prex 5355 |
. . . . . . . 8
⊢ {𝐵, 𝐶} ∈ V |
19 | | dmsnopg 6116 |
. . . . . . . 8
⊢ ({𝐵, 𝐶} ∈ V → dom {〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
20 | 18, 19 | mp1i 13 |
. . . . . . 7
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom {〈𝐴, {𝐵, 𝐶}〉} = {𝐴}) |
21 | 17, 20 | eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → dom (iEdg‘𝐺) = {𝐴}) |
22 | | fveq1 6773 |
. . . . . . . 8
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → ((iEdg‘𝐺)‘𝑥) = ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)) |
23 | 22 | eleq2d 2824 |
. . . . . . 7
⊢
((iEdg‘𝐺) =
{〈𝐴, {𝐵, 𝐶}〉} → (𝐵 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥))) |
24 | 23 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (𝐵 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥))) |
25 | 21, 24 | rabeqbidv 3420 |
. . . . 5
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) |
26 | 25 | fveq2d 6778 |
. . . 4
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)})) |
27 | | fveq2 6774 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥) = ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴)) |
28 | 27 | eleq2d 2824 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥) ↔ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴))) |
29 | 28 | rabsnif 4659 |
. . . . . . . 8
⊢ {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)} = if(𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴), {𝐴}, ∅) |
30 | | prid1g 4696 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵, 𝐶}) |
31 | 3, 30 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ {𝐵, 𝐶}) |
32 | | fvsng 7052 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ {𝐵, 𝐶} ∈ V) → ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴) = {𝐵, 𝐶}) |
33 | 2, 18, 32 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴) = {𝐵, 𝐶}) |
34 | 31, 33 | eleqtrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴)) |
35 | 34 | iftrued 4467 |
. . . . . . . 8
⊢ (𝜑 → if(𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝐴), {𝐴}, ∅) = {𝐴}) |
36 | 29, 35 | eqtrid 2790 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)} = {𝐴}) |
37 | 36 | fveq2d 6778 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = (♯‘{𝐴})) |
38 | | hashsng 14084 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → (♯‘{𝐴}) = 1) |
39 | 2, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘{𝐴}) = 1) |
40 | 37, 39 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = 1) |
41 | 40 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐵 ∈ ({〈𝐴, {𝐵, 𝐶}〉}‘𝑥)}) = 1) |
42 | 26, 41 | eqtrd 2778 |
. . 3
⊢ ((𝜑 ∧ (iEdg‘𝐺) = {〈𝐴, {𝐵, 𝐶}〉}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
43 | 8, 42 | mpdan 684 |
. 2
⊢ (𝜑 → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐵 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
44 | 15, 43 | eqtrd 2778 |
1
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1) |