Step | Hyp | Ref
| Expression |
1 | | 1hevtxdg0.i |
. . . 4
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
2 | 1 | dmeqd 5571 |
. . 3
⊢ (𝜑 → dom (iEdg‘𝐺) = dom {〈𝐴, 𝐸〉}) |
3 | | 1hevtxdg1.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) |
4 | | dmsnopg 5860 |
. . . 4
⊢ (𝐸 ∈ 𝒫 𝑉 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
6 | 2, 5 | eqtrd 2814 |
. 2
⊢ (𝜑 → dom (iEdg‘𝐺) = {𝐴}) |
7 | | 1hevtxdg0.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | 1hevtxdg0.v |
. . . . . . . . . 10
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) |
9 | 8 | pweqd 4384 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
10 | 3, 9 | eleqtrrd 2862 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ 𝒫 (Vtx‘𝐺)) |
11 | | 1hevtxdg1.l |
. . . . . . . 8
⊢ (𝜑 → 2 ≤
(♯‘𝐸)) |
12 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → (♯‘𝑥) = (♯‘𝐸)) |
13 | 12 | breq2d 4898 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → (2 ≤ (♯‘𝑥) ↔ 2 ≤
(♯‘𝐸))) |
14 | 13 | elrab 3572 |
. . . . . . . 8
⊢ (𝐸 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)} ↔
(𝐸 ∈ 𝒫
(Vtx‘𝐺) ∧ 2 ≤
(♯‘𝐸))) |
15 | 10, 11, 14 | sylanbrc 578 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
16 | 7, 15 | fsnd 6433 |
. . . . . 6
⊢ (𝜑 → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
17 | 16 | adantr 474 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
18 | 1 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
19 | | simpr 479 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → dom (iEdg‘𝐺) = {𝐴}) |
20 | 18, 19 | feq12d 6279 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)} ↔
{〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)})) |
21 | 17, 20 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)}) |
22 | | 1hevtxdg0.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
23 | 22, 8 | eleqtrrd 2862 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (Vtx‘𝐺)) |
24 | 23 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → 𝐷 ∈ (Vtx‘𝐺)) |
25 | | eqid 2778 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
26 | | eqid 2778 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
27 | | eqid 2778 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
28 | | eqid 2778 |
. . . . 5
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
29 | 25, 26, 27, 28 | vtxdlfgrval 26833 |
. . . 4
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤
(♯‘𝑥)} ∧
𝐷 ∈ (Vtx‘𝐺)) → ((VtxDeg‘𝐺)‘𝐷) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
30 | 21, 24, 29 | syl2anc 579 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
31 | | rabeq 3389 |
. . . . 5
⊢ (dom
(iEdg‘𝐺) = {𝐴} → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
32 | 31 | adantl 475 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
33 | 32 | fveq2d 6450 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
34 | | fveq2 6446 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝐴)) |
35 | 34 | eleq2d 2845 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐷 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐷 ∈ ((iEdg‘𝐺)‘𝐴))) |
36 | 35 | rabsnif 4490 |
. . . . . . 7
⊢ {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) |
37 | | 1hevtxdg1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝐸) |
38 | 1 | fveq1d 6448 |
. . . . . . . . . 10
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = ({〈𝐴, 𝐸〉}‘𝐴)) |
39 | | fvsng 6713 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝒫 𝑉) → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
40 | 7, 3, 39 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
41 | 38, 40 | eqtrd 2814 |
. . . . . . . . 9
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = 𝐸) |
42 | 37, 41 | eleqtrrd 2862 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((iEdg‘𝐺)‘𝐴)) |
43 | 42 | iftrued 4315 |
. . . . . . 7
⊢ (𝜑 → if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) = {𝐴}) |
44 | 36, 43 | syl5eq 2826 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝐴}) |
45 | 44 | fveq2d 6450 |
. . . . 5
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (♯‘{𝐴})) |
46 | | hashsng 13474 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → (♯‘{𝐴}) = 1) |
47 | 7, 46 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘{𝐴}) = 1) |
48 | 45, 47 | eqtrd 2814 |
. . . 4
⊢ (𝜑 → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
49 | 48 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (♯‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
50 | 30, 33, 49 | 3eqtrd 2818 |
. 2
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = 1) |
51 | 6, 50 | mpdan 677 |
1
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1) |