Step | Hyp | Ref
| Expression |
1 | | 1hevtxdg0.i |
. . . 4
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
2 | 1 | dmeqd 5814 |
. . 3
⊢ (𝜑 → dom (iEdg‘𝐺) = dom {〈𝐴, 𝐸〉}) |
3 | | 1hevtxdg1.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) |
4 | | dmsnopg 6116 |
. . . 4
⊢ (𝐸 ∈ 𝒫 𝑉 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
6 | 2, 5 | eqtrd 2778 |
. 2
⊢ (𝜑 → dom (iEdg‘𝐺) = {𝐴}) |
7 | | 1hevtxdg0.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → (♯‘𝑥) = (♯‘𝐸)) |
9 | 8 | breq2d 5086 |
. . . . . . . 8
⊢ (𝑥 = 𝐸 → (2 ≤ (♯‘𝑥) ↔ 2 ≤
(♯‘𝐸))) |
10 | | 1hevtxdg0.v |
. . . . . . . . . 10
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) |
11 | 10 | pweqd 4552 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
12 | 3, 11 | eleqtrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ 𝒫 (Vtx‘𝐺)) |
13 | | 1hevtxdg1.l |
. . . . . . . 8
⊢ (𝜑 → 2 ≤
(♯‘𝐸)) |
14 | 9, 12, 13 | elrabd 3626 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
15 | 7, 14 | fsnd 6759 |
. . . . . 6
⊢ (𝜑 → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
16 | 15 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
17 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
18 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → dom (iEdg‘𝐺) = {𝐴}) |
19 | 17, 18 | feq12d 6588 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)} ↔
{〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)})) |
20 | 16, 19 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
21 | | 1hevtxdg0.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
22 | 21, 10 | eleqtrrd 2842 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (Vtx‘𝐺)) |
23 | 22 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → 𝐷 ∈ (Vtx‘𝐺)) |
24 | | eqid 2738 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
25 | | eqid 2738 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
26 | | eqid 2738 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
27 | | eqid 2738 |
. . . . 5
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
28 | 24, 25, 26, 27 | vtxdlfgrval 27852 |
. . . 4
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)} ∧
𝐷 ∈ (Vtx‘𝐺)) → ((VtxDeg‘𝐺)‘𝐷) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
29 | 20, 23, 28 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
30 | | rabeq 3418 |
. . . . 5
⊢ (dom
(iEdg‘𝐺) = {𝐴} → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
31 | 30 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
32 | 31 | fveq2d 6778 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
33 | | fveq2 6774 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝐴)) |
34 | 33 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐷 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐷 ∈ ((iEdg‘𝐺)‘𝐴))) |
35 | 34 | rabsnif 4659 |
. . . . . . 7
⊢ {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) |
36 | | 1hevtxdg1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝐸) |
37 | 1 | fveq1d 6776 |
. . . . . . . . . 10
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = ({〈𝐴, 𝐸〉}‘𝐴)) |
38 | | fvsng 7052 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝒫 𝑉) → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
39 | 7, 3, 38 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
40 | 37, 39 | eqtrd 2778 |
. . . . . . . . 9
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = 𝐸) |
41 | 36, 40 | eleqtrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((iEdg‘𝐺)‘𝐴)) |
42 | 41 | iftrued 4467 |
. . . . . . 7
⊢ (𝜑 → if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) = {𝐴}) |
43 | 35, 42 | eqtrid 2790 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝐴}) |
44 | 43 | fveq2d 6778 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝐴})) |
45 | | hashsng 14084 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → (♯‘{𝐴}) = 1) |
46 | 7, 45 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝐴}) = 1) |
47 | 44, 46 | eqtrd 2778 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
48 | 47 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
49 | 29, 32, 48 | 3eqtrd 2782 |
. 2
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = 1) |
50 | 6, 49 | mpdan 684 |
1
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1) |