Step | Hyp | Ref
| Expression |
1 | | frgrusgr 29247 |
. . . . . 6
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
2 | 1 | anim1i 616 |
. . . . 5
β’ ((πΊ β FriendGraph β§ π β π) β (πΊ β USGraph β§ π β π)) |
3 | 2 | adantr 482 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β (πΊ β USGraph β§ π β π)) |
4 | | vdn1frgrv2.v |
. . . . 5
β’ π = (VtxβπΊ) |
5 | | eqid 2737 |
. . . . 5
β’
(iEdgβπΊ) =
(iEdgβπΊ) |
6 | | eqid 2737 |
. . . . 5
β’ dom
(iEdgβπΊ) = dom
(iEdgβπΊ) |
7 | | eqid 2737 |
. . . . 5
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
8 | 4, 5, 6, 7 | vtxdusgrval 28477 |
. . . 4
β’ ((πΊ β USGraph β§ π β π) β ((VtxDegβπΊ)βπ) = (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)})) |
9 | 3, 8 | syl 17 |
. . 3
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β ((VtxDegβπΊ)βπ) = (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)})) |
10 | | eqid 2737 |
. . . . . . 7
β’
(EdgβπΊ) =
(EdgβπΊ) |
11 | 4, 10 | 3cyclfrgrrn2 29273 |
. . . . . 6
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
12 | 11 | adantlr 714 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
13 | | preq1 4699 |
. . . . . . . . . . . . . . . 16
β’ (π = π β {π, π} = {π, π}) |
14 | 13 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = π β ({π, π} β (EdgβπΊ) β {π, π} β (EdgβπΊ))) |
15 | | preq2 4700 |
. . . . . . . . . . . . . . . 16
β’ (π = π β {π, π} = {π, π}) |
16 | 15 | eleq1d 2823 |
. . . . . . . . . . . . . . 15
β’ (π = π β ({π, π} β (EdgβπΊ) β {π, π} β (EdgβπΊ))) |
17 | 14, 16 | 3anbi13d 1439 |
. . . . . . . . . . . . . 14
β’ (π = π β (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
18 | 17 | anbi2d 630 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))))) |
19 | 18 | 2rexbidv 3214 |
. . . . . . . . . . . 12
β’ (π = π β (βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))))) |
20 | 19 | rspcva 3582 |
. . . . . . . . . . 11
β’ ((π β π β§ βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) β βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) |
21 | 1 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β§ πΊ β FriendGraph ) β πΊ β
USGraph) |
22 | | simplll 774 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β§ πΊ β FriendGraph ) β π β π) |
23 | | 3simpb 1150 |
. . . . . . . . . . . . . . . . . 18
β’ (({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
24 | 23 | ad3antlr 730 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β§ πΊ β FriendGraph ) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
25 | 5, 10 | usgr2edg1 28202 |
. . . . . . . . . . . . . . . . 17
β’ (((πΊ β USGraph β§ π β π) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)) |
26 | 21, 22, 24, 25 | syl21anc 837 |
. . . . . . . . . . . . . . . 16
β’ ((((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β§ πΊ β FriendGraph ) β Β¬
β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)) |
27 | 26 | a1d 25 |
. . . . . . . . . . . . . . 15
β’ ((((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β§ πΊ β FriendGraph ) β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
28 | 27 | ex 414 |
. . . . . . . . . . . . . 14
β’ (((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ π β π) β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)))) |
29 | 28 | ex 414 |
. . . . . . . . . . . . 13
β’ ((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (π β π β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
30 | 29 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β π β§ π β π) β ((π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (π β π β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)))))) |
31 | 30 | rexlimivv 3197 |
. . . . . . . . . . 11
β’
(βπ β
π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (π β π β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
32 | 20, 31 | syl 17 |
. . . . . . . . . 10
β’ ((π β π β§ βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)))) β (π β π β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
33 | 32 | ex 414 |
. . . . . . . . 9
β’ (π β π β (βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (π β π β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)))))) |
34 | 33 | pm2.43a 54 |
. . . . . . . 8
β’ (π β π β (βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β (πΊ β FriendGraph β (1 <
(β―βπ) β
Β¬ β!π₯ β dom
(iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
35 | 34 | com24 95 |
. . . . . . 7
β’ (π β π β (1 < (β―βπ) β (πΊ β FriendGraph β (βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
36 | 35 | com3r 87 |
. . . . . 6
β’ (πΊ β FriendGraph β
(π β π β (1 < (β―βπ) β (βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))))) |
37 | 36 | imp31 419 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β (βπ β π βπ β π βπ β π (π β π β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
38 | 12, 37 | mpd 15 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯)) |
39 | | fvex 6860 |
. . . . . . . . 9
β’
(iEdgβπΊ)
β V |
40 | 39 | dmex 7853 |
. . . . . . . 8
β’ dom
(iEdgβπΊ) β
V |
41 | 40 | a1i 11 |
. . . . . . 7
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β dom (iEdgβπΊ) β V) |
42 | | rabexg 5293 |
. . . . . . 7
β’ (dom
(iEdgβπΊ) β V
β {π₯ β dom
(iEdgβπΊ) β£
π β ((iEdgβπΊ)βπ₯)} β V) |
43 | | hash1snb 14326 |
. . . . . . 7
β’ ({π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} β V β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) = 1 β βπ{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = {π})) |
44 | 41, 42, 43 | 3syl 18 |
. . . . . 6
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) = 1 β βπ{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = {π})) |
45 | | reusn 4693 |
. . . . . 6
β’
(β!π₯ β
dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯) β βπ{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)} = {π}) |
46 | 44, 45 | bitr4di 289 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) = 1 β β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
47 | 46 | necon3abid 2981 |
. . . 4
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β ((β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) β 1 β Β¬ β!π₯ β dom (iEdgβπΊ)π β ((iEdgβπΊ)βπ₯))) |
48 | 38, 47 | mpbird 257 |
. . 3
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β (β―β{π₯ β dom (iEdgβπΊ) β£ π β ((iEdgβπΊ)βπ₯)}) β 1) |
49 | 9, 48 | eqnetrd 3012 |
. 2
β’ (((πΊ β FriendGraph β§ π β π) β§ 1 < (β―βπ)) β ((VtxDegβπΊ)βπ) β 1) |
50 | 49 | ex 414 |
1
β’ ((πΊ β FriendGraph β§ π β π) β (1 < (β―βπ) β ((VtxDegβπΊ)βπ) β 1)) |