Step |
Hyp |
Ref |
Expression |
1 |
|
1loopgruspgr.v |
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
2 |
|
1loopgruspgr.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) |
3 |
|
1loopgruspgr.n |
⊢ ( 𝜑 → 𝑁 ∈ 𝑉 ) |
4 |
|
1loopgruspgr.i |
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , { 𝑁 } 〉 } ) |
5 |
1 2 3 4
|
1loopgruspgr |
⊢ ( 𝜑 → 𝐺 ∈ USPGraph ) |
6 |
|
uspgrushgr |
⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph ) |
7 |
5 6
|
syl |
⊢ ( 𝜑 → 𝐺 ∈ USHGraph ) |
8 |
3 1
|
eleqtrrd |
⊢ ( 𝜑 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) |
9 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
10 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
11 |
|
eqid |
⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 ) |
12 |
9 10 11
|
vtxdushgrfvedg |
⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) ) |
13 |
7 8 12
|
syl2anc |
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) ) |
14 |
|
snex |
⊢ { 𝑁 } ∈ V |
15 |
|
sneq |
⊢ ( 𝑎 = { 𝑁 } → { 𝑎 } = { { 𝑁 } } ) |
16 |
15
|
eqeq2d |
⊢ ( 𝑎 = { 𝑁 } → ( { { 𝑁 } } = { 𝑎 } ↔ { { 𝑁 } } = { { 𝑁 } } ) ) |
17 |
|
eqid |
⊢ { { 𝑁 } } = { { 𝑁 } } |
18 |
14 16 17
|
ceqsexv2d |
⊢ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } |
19 |
18
|
a1i |
⊢ ( 𝜑 → ∃ 𝑎 { { 𝑁 } } = { 𝑎 } ) |
20 |
|
snidg |
⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ { 𝑁 } ) |
21 |
3 20
|
syl |
⊢ ( 𝜑 → 𝑁 ∈ { 𝑁 } ) |
22 |
21
|
iftrued |
⊢ ( 𝜑 → if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } } ) |
23 |
22
|
eqeq1d |
⊢ ( 𝜑 → ( if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } ) ) |
24 |
23
|
exbidv |
⊢ ( 𝜑 → ( ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } ) ) |
25 |
19 24
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) |
26 |
1 2 3 4
|
1loopgredg |
⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝑁 } } ) |
27 |
26
|
rabeqdv |
⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁 ∈ 𝑒 } ) |
28 |
|
eleq2 |
⊢ ( 𝑒 = { 𝑁 } → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ { 𝑁 } ) ) |
29 |
28
|
rabsnif |
⊢ { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁 ∈ 𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) |
30 |
27 29
|
eqtrdi |
⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) ) |
31 |
30
|
eqeq1d |
⊢ ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ↔ if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) ) |
32 |
31
|
exbidv |
⊢ ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ↔ ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) ) |
33 |
25 32
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ) |
34 |
|
fvex |
⊢ ( Edg ‘ 𝐺 ) ∈ V |
35 |
34
|
rabex |
⊢ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ∈ V |
36 |
|
hash1snb |
⊢ ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ) ) |
37 |
35 36
|
ax-mp |
⊢ ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ) |
38 |
33 37
|
sylibr |
⊢ ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 ) |
39 |
|
eqid |
⊢ { 𝑁 } = { 𝑁 } |
40 |
39
|
iftruei |
⊢ if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } } |
41 |
40
|
eqeq1i |
⊢ ( if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } ) |
42 |
41
|
exbii |
⊢ ( ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } ) |
43 |
19 42
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) |
44 |
26
|
rabeqdv |
⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } ) |
45 |
|
eqeq1 |
⊢ ( 𝑒 = { 𝑁 } → ( 𝑒 = { 𝑁 } ↔ { 𝑁 } = { 𝑁 } ) ) |
46 |
45
|
rabsnif |
⊢ { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) |
47 |
44 46
|
eqtrdi |
⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) ) |
48 |
47
|
eqeq1d |
⊢ ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) ) |
49 |
48
|
exbidv |
⊢ ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) ) |
50 |
43 49
|
mpbird |
⊢ ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ) |
51 |
34
|
rabex |
⊢ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V |
52 |
|
hash1snb |
⊢ ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ) ) |
53 |
51 52
|
ax-mp |
⊢ ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ) |
54 |
50 53
|
sylibr |
⊢ ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ) |
55 |
38 54
|
oveq12d |
⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) = ( 1 +𝑒 1 ) ) |
56 |
|
1re |
⊢ 1 ∈ ℝ |
57 |
|
rexadd |
⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 +𝑒 1 ) = ( 1 + 1 ) ) |
58 |
56 56 57
|
mp2an |
⊢ ( 1 +𝑒 1 ) = ( 1 + 1 ) |
59 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
60 |
58 59
|
eqtri |
⊢ ( 1 +𝑒 1 ) = 2 |
61 |
60
|
a1i |
⊢ ( 𝜑 → ( 1 +𝑒 1 ) = 2 ) |
62 |
13 55 61
|
3eqtrd |
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 ) |