Step | Hyp | Ref
| Expression |
1 | | 1egrvtxdg1.v |
. . . . 5
β’ (π β (VtxβπΊ) = π) |
2 | 1 | adantl 483 |
. . . 4
β’ ((π΅ = π· β§ π) β (VtxβπΊ) = π) |
3 | | 1egrvtxdg1.a |
. . . . 5
β’ (π β π΄ β π) |
4 | 3 | adantl 483 |
. . . 4
β’ ((π΅ = π· β§ π) β π΄ β π) |
5 | | 1egrvtxdg1.b |
. . . . 5
β’ (π β π΅ β π) |
6 | 5 | adantl 483 |
. . . 4
β’ ((π΅ = π· β§ π) β π΅ β π) |
7 | | 1egrvtxdg0.i |
. . . . . 6
β’ (π β (iEdgβπΊ) = {β¨π΄, {π΅, π·}β©}) |
8 | 7 | adantl 483 |
. . . . 5
β’ ((π΅ = π· β§ π) β (iEdgβπΊ) = {β¨π΄, {π΅, π·}β©}) |
9 | | preq2 4696 |
. . . . . . . . . 10
β’ (π· = π΅ β {π΅, π·} = {π΅, π΅}) |
10 | 9 | eqcoms 2741 |
. . . . . . . . 9
β’ (π΅ = π· β {π΅, π·} = {π΅, π΅}) |
11 | | dfsn2 4600 |
. . . . . . . . 9
β’ {π΅} = {π΅, π΅} |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . 8
β’ (π΅ = π· β {π΅, π·} = {π΅}) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ ((π΅ = π· β§ π) β {π΅, π·} = {π΅}) |
14 | 13 | opeq2d 4838 |
. . . . . 6
β’ ((π΅ = π· β§ π) β β¨π΄, {π΅, π·}β© = β¨π΄, {π΅}β©) |
15 | 14 | sneqd 4599 |
. . . . 5
β’ ((π΅ = π· β§ π) β {β¨π΄, {π΅, π·}β©} = {β¨π΄, {π΅}β©}) |
16 | 8, 15 | eqtrd 2773 |
. . . 4
β’ ((π΅ = π· β§ π) β (iEdgβπΊ) = {β¨π΄, {π΅}β©}) |
17 | | 1egrvtxdg1.c |
. . . . . . 7
β’ (π β πΆ β π) |
18 | | 1egrvtxdg1.n |
. . . . . . . 8
β’ (π β π΅ β πΆ) |
19 | 18 | necomd 2996 |
. . . . . . 7
β’ (π β πΆ β π΅) |
20 | 17, 19 | jca 513 |
. . . . . 6
β’ (π β (πΆ β π β§ πΆ β π΅)) |
21 | | eldifsn 4748 |
. . . . . 6
β’ (πΆ β (π β {π΅}) β (πΆ β π β§ πΆ β π΅)) |
22 | 20, 21 | sylibr 233 |
. . . . 5
β’ (π β πΆ β (π β {π΅})) |
23 | 22 | adantl 483 |
. . . 4
β’ ((π΅ = π· β§ π) β πΆ β (π β {π΅})) |
24 | 2, 4, 6, 16, 23 | 1loopgrvd0 28494 |
. . 3
β’ ((π΅ = π· β§ π) β ((VtxDegβπΊ)βπΆ) = 0) |
25 | 24 | ex 414 |
. 2
β’ (π΅ = π· β (π β ((VtxDegβπΊ)βπΆ) = 0)) |
26 | | necom 2994 |
. . . . . . . . . 10
β’ (π΅ β πΆ β πΆ β π΅) |
27 | | df-ne 2941 |
. . . . . . . . . 10
β’ (πΆ β π΅ β Β¬ πΆ = π΅) |
28 | 26, 27 | sylbb 218 |
. . . . . . . . 9
β’ (π΅ β πΆ β Β¬ πΆ = π΅) |
29 | 18, 28 | syl 17 |
. . . . . . . 8
β’ (π β Β¬ πΆ = π΅) |
30 | | 1egrvtxdg0.n |
. . . . . . . . 9
β’ (π β πΆ β π·) |
31 | 30 | neneqd 2945 |
. . . . . . . 8
β’ (π β Β¬ πΆ = π·) |
32 | 29, 31 | jca 513 |
. . . . . . 7
β’ (π β (Β¬ πΆ = π΅ β§ Β¬ πΆ = π·)) |
33 | 32 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β (Β¬ πΆ = π΅ β§ Β¬ πΆ = π·)) |
34 | | ioran 983 |
. . . . . 6
β’ (Β¬
(πΆ = π΅ β¨ πΆ = π·) β (Β¬ πΆ = π΅ β§ Β¬ πΆ = π·)) |
35 | 33, 34 | sylibr 233 |
. . . . 5
β’ ((π΅ β π· β§ π) β Β¬ (πΆ = π΅ β¨ πΆ = π·)) |
36 | | edgval 28042 |
. . . . . . . . 9
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
37 | 7 | rneqd 5894 |
. . . . . . . . . 10
β’ (π β ran (iEdgβπΊ) = ran {β¨π΄, {π΅, π·}β©}) |
38 | | rnsnopg 6174 |
. . . . . . . . . . 11
β’ (π΄ β π β ran {β¨π΄, {π΅, π·}β©} = {{π΅, π·}}) |
39 | 3, 38 | syl 17 |
. . . . . . . . . 10
β’ (π β ran {β¨π΄, {π΅, π·}β©} = {{π΅, π·}}) |
40 | 37, 39 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β ran (iEdgβπΊ) = {{π΅, π·}}) |
41 | 36, 40 | eqtrid 2785 |
. . . . . . . 8
β’ (π β (EdgβπΊ) = {{π΅, π·}}) |
42 | 41 | adantl 483 |
. . . . . . 7
β’ ((π΅ β π· β§ π) β (EdgβπΊ) = {{π΅, π·}}) |
43 | 42 | rexeqdv 3313 |
. . . . . 6
β’ ((π΅ β π· β§ π) β (βπ β (EdgβπΊ)πΆ β π β βπ β {{π΅, π·}}πΆ β π)) |
44 | | prex 5390 |
. . . . . . 7
β’ {π΅, π·} β V |
45 | | eleq2 2823 |
. . . . . . . 8
β’ (π = {π΅, π·} β (πΆ β π β πΆ β {π΅, π·})) |
46 | 45 | rexsng 4636 |
. . . . . . 7
β’ ({π΅, π·} β V β (βπ β {{π΅, π·}}πΆ β π β πΆ β {π΅, π·})) |
47 | 44, 46 | mp1i 13 |
. . . . . 6
β’ ((π΅ β π· β§ π) β (βπ β {{π΅, π·}}πΆ β π β πΆ β {π΅, π·})) |
48 | | elprg 4608 |
. . . . . . . 8
β’ (πΆ β π β (πΆ β {π΅, π·} β (πΆ = π΅ β¨ πΆ = π·))) |
49 | 17, 48 | syl 17 |
. . . . . . 7
β’ (π β (πΆ β {π΅, π·} β (πΆ = π΅ β¨ πΆ = π·))) |
50 | 49 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β (πΆ β {π΅, π·} β (πΆ = π΅ β¨ πΆ = π·))) |
51 | 43, 47, 50 | 3bitrd 305 |
. . . . 5
β’ ((π΅ β π· β§ π) β (βπ β (EdgβπΊ)πΆ β π β (πΆ = π΅ β¨ πΆ = π·))) |
52 | 35, 51 | mtbird 325 |
. . . 4
β’ ((π΅ β π· β§ π) β Β¬ βπ β (EdgβπΊ)πΆ β π) |
53 | | eqid 2733 |
. . . . . 6
β’
(VtxβπΊ) =
(VtxβπΊ) |
54 | 3 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β π΄ β π) |
55 | 5, 1 | eleqtrrd 2837 |
. . . . . . 7
β’ (π β π΅ β (VtxβπΊ)) |
56 | 55 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β π΅ β (VtxβπΊ)) |
57 | | 1egrvtxdg0.d |
. . . . . . . 8
β’ (π β π· β π) |
58 | 57, 1 | eleqtrrd 2837 |
. . . . . . 7
β’ (π β π· β (VtxβπΊ)) |
59 | 58 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β π· β (VtxβπΊ)) |
60 | 7 | adantl 483 |
. . . . . 6
β’ ((π΅ β π· β§ π) β (iEdgβπΊ) = {β¨π΄, {π΅, π·}β©}) |
61 | | simpl 484 |
. . . . . 6
β’ ((π΅ β π· β§ π) β π΅ β π·) |
62 | 53, 54, 56, 59, 60, 61 | usgr1e 28235 |
. . . . 5
β’ ((π΅ β π· β§ π) β πΊ β USGraph) |
63 | 17, 1 | eleqtrrd 2837 |
. . . . . 6
β’ (π β πΆ β (VtxβπΊ)) |
64 | 63 | adantl 483 |
. . . . 5
β’ ((π΅ β π· β§ π) β πΆ β (VtxβπΊ)) |
65 | | eqid 2733 |
. . . . . 6
β’
(EdgβπΊ) =
(EdgβπΊ) |
66 | | eqid 2733 |
. . . . . 6
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
67 | 53, 65, 66 | vtxdusgr0edgnel 28485 |
. . . . 5
β’ ((πΊ β USGraph β§ πΆ β (VtxβπΊ)) β (((VtxDegβπΊ)βπΆ) = 0 β Β¬ βπ β (EdgβπΊ)πΆ β π)) |
68 | 62, 64, 67 | syl2anc 585 |
. . . 4
β’ ((π΅ β π· β§ π) β (((VtxDegβπΊ)βπΆ) = 0 β Β¬ βπ β (EdgβπΊ)πΆ β π)) |
69 | 52, 68 | mpbird 257 |
. . 3
β’ ((π΅ β π· β§ π) β ((VtxDegβπΊ)βπΆ) = 0) |
70 | 69 | ex 414 |
. 2
β’ (π΅ β π· β (π β ((VtxDegβπΊ)βπΆ) = 0)) |
71 | 25, 70 | pm2.61ine 3025 |
1
β’ (π β ((VtxDegβπΊ)βπΆ) = 0) |