Step | Hyp | Ref
| Expression |
1 | | 1hevtxdg0.i |
. . . 4
⊢ (𝜑 → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
2 | 1 | dmeqd 5248 |
. . 3
⊢ (𝜑 → dom (iEdg‘𝐺) = dom {〈𝐴, 𝐸〉}) |
3 | | 1hevtxdg1.e |
. . . 4
⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉) |
4 | | dmsnopg 5524 |
. . . 4
⊢ (𝐸 ∈ 𝒫 𝑉 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → dom {〈𝐴, 𝐸〉} = {𝐴}) |
6 | 2, 5 | eqtrd 2644 |
. 2
⊢ (𝜑 → dom (iEdg‘𝐺) = {𝐴}) |
7 | | 1hevtxdg0.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
8 | | 1hevtxdg0.v |
. . . . . . . . . 10
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉) |
9 | 8 | pweqd 4113 |
. . . . . . . . 9
⊢ (𝜑 → 𝒫 (Vtx‘𝐺) = 𝒫 𝑉) |
10 | 3, 9 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ 𝒫 (Vtx‘𝐺)) |
11 | | 1hevtxdg1.l |
. . . . . . . 8
⊢ (𝜑 → 2 ≤ (#‘𝐸)) |
12 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐸 → (#‘𝑥) = (#‘𝐸)) |
13 | 12 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑥 = 𝐸 → (2 ≤ (#‘𝑥) ↔ 2 ≤ (#‘𝐸))) |
14 | 13 | elrab 3331 |
. . . . . . . 8
⊢ (𝐸 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)} ↔ (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 2 ≤ (#‘𝐸))) |
15 | 10, 11, 14 | sylanbrc 695 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)}) |
16 | 7, 15 | fsnd 6091 |
. . . . . 6
⊢ (𝜑 → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)}) |
17 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)}) |
18 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺) = {〈𝐴, 𝐸〉}) |
19 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → dom (iEdg‘𝐺) = {𝐴}) |
20 | 18, 19 | feq12d 5946 |
. . . . 5
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)} ↔ {〈𝐴, 𝐸〉}:{𝐴}⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)})) |
21 | 17, 20 | mpbird 246 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)}) |
22 | | 1hevtxdg0.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
23 | 22, 8 | eleqtrrd 2691 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ (Vtx‘𝐺)) |
24 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → 𝐷 ∈ (Vtx‘𝐺)) |
25 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
26 | | eqid 2610 |
. . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
27 | | eqid 2610 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
28 | | eqid 2610 |
. . . . 5
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
29 | 25, 26, 27, 28 | vtxdlfgrval 40700 |
. . . 4
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ 2 ≤ (#‘𝑥)} ∧ 𝐷 ∈ (Vtx‘𝐺)) → ((VtxDeg‘𝐺)‘𝐷) = (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
30 | 21, 24, 29 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
31 | | rabeq 3166 |
. . . . 5
⊢ (dom
(iEdg‘𝐺) = {𝐴} → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
32 | 31 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) |
33 | 32 | fveq2d 6107 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (#‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (#‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)})) |
34 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝐺)‘𝐴)) |
35 | 34 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐷 ∈ ((iEdg‘𝐺)‘𝑥) ↔ 𝐷 ∈ ((iEdg‘𝐺)‘𝐴))) |
36 | 35 | rabsnif 4202 |
. . . . . . 7
⊢ {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) |
37 | | 1hevtxdg1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ 𝐸) |
38 | 1 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = ({〈𝐴, 𝐸〉}‘𝐴)) |
39 | | fvsng 6352 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝒫 𝑉) → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
40 | 7, 3, 39 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, 𝐸〉}‘𝐴) = 𝐸) |
41 | 38, 40 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((iEdg‘𝐺)‘𝐴) = 𝐸) |
42 | 37, 41 | eleqtrrd 2691 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ((iEdg‘𝐺)‘𝐴)) |
43 | 42 | iftrued 4044 |
. . . . . . 7
⊢ (𝜑 → if(𝐷 ∈ ((iEdg‘𝐺)‘𝐴), {𝐴}, ∅) = {𝐴}) |
44 | 36, 43 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)} = {𝐴}) |
45 | 44 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = (#‘{𝐴})) |
46 | | hashsng 13020 |
. . . . . 6
⊢ (𝐴 ∈ 𝑋 → (#‘{𝐴}) = 1) |
47 | 7, 46 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝐴}) = 1) |
48 | 45, 47 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
49 | 48 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → (#‘{𝑥 ∈ {𝐴} ∣ 𝐷 ∈ ((iEdg‘𝐺)‘𝑥)}) = 1) |
50 | 30, 33, 49 | 3eqtrd 2648 |
. 2
⊢ ((𝜑 ∧ dom (iEdg‘𝐺) = {𝐴}) → ((VtxDeg‘𝐺)‘𝐷) = 1) |
51 | 6, 50 | mpdan 699 |
1
⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐷) = 1) |