Step | Hyp | Ref
| Expression |
1 | | frgrusgr 29247 |
. . . . 5
β’ (πΊ β FriendGraph β πΊ β
USGraph) |
2 | | usgrupgr 28175 |
. . . . 5
β’ (πΊ β USGraph β πΊ β
UPGraph) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (πΊ β FriendGraph β πΊ β
UPGraph) |
4 | | eqid 2737 |
. . . . . . . . 9
β’
(VtxβπΊ) =
(VtxβπΊ) |
5 | | eqid 2737 |
. . . . . . . . 9
β’
(EdgβπΊ) =
(EdgβπΊ) |
6 | 4, 5 | upgr4cycl4dv4e 29171 |
. . . . . . . 8
β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 4) β βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπ β (VtxβπΊ)((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) |
7 | 4, 5 | isfrgr 29246 |
. . . . . . . . . . . 12
β’ (πΊ β FriendGraph β
(πΊ β USGraph β§
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
8 | | simplrl 776 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β (VtxβπΊ)) |
9 | | necom 2998 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β π β π) |
10 | 9 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β π β π) |
11 | 10 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β π β§ π β π β§ π β π) β π β π) |
12 | 11 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’
(((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β π β π) |
13 | 12 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β π) |
14 | | eldifsn 4752 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((VtxβπΊ) β {π}) β (π β (VtxβπΊ) β§ π β π)) |
15 | 8, 13, 14 | sylanbrc 584 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β ((VtxβπΊ) β {π})) |
16 | | sneq 4601 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β {π} = {π}) |
17 | 16 | difeq2d 4087 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β ((VtxβπΊ) β {π}) = ((VtxβπΊ) β {π})) |
18 | | preq2 4700 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = π β {π₯, π} = {π₯, π}) |
19 | 18 | preq1d 4705 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β {{π₯, π}, {π₯, π}} = {{π₯, π}, {π₯, π}}) |
20 | 19 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ({{π₯, π}, {π₯, π}} β (EdgβπΊ) β {{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
21 | 20 | reubidv 3374 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
22 | 17, 21 | raleqbidv 3322 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
23 | 22 | rspcv 3580 |
. . . . . . . . . . . . . . . . 17
β’ (π β (VtxβπΊ) β (βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
24 | 23 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
25 | | preq2 4700 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β {π₯, π} = {π₯, π}) |
26 | 25 | preq2d 4706 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β {{π₯, π}, {π₯, π}} = {{π₯, π}, {π₯, π}}) |
27 | 26 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β ({{π₯, π}, {π₯, π}} β (EdgβπΊ) β {{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
28 | 27 | reubidv 3374 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
29 | 28 | rspcv 3580 |
. . . . . . . . . . . . . . . 16
β’ (π β ((VtxβπΊ) β {π}) β (βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
30 | 15, 24, 29 | sylsyld 61 |
. . . . . . . . . . . . . . 15
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ))) |
31 | | prcom 4698 |
. . . . . . . . . . . . . . . . . . 19
β’ {π₯, π} = {π, π₯} |
32 | 31 | preq1i 4702 |
. . . . . . . . . . . . . . . . . 18
β’ {{π₯, π}, {π₯, π}} = {{π, π₯}, {π₯, π}} |
33 | 32 | sseq1i 3977 |
. . . . . . . . . . . . . . . . 17
β’ ({{π₯, π}, {π₯, π}} β (EdgβπΊ) β {{π, π₯}, {π₯, π}} β (EdgβπΊ)) |
34 | 33 | reubii 3365 |
. . . . . . . . . . . . . . . 16
β’
(β!π₯ β
(VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β β!π₯ β (VtxβπΊ){{π, π₯}, {π₯, π}} β (EdgβπΊ)) |
35 | | simprll 778 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
36 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) |
37 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β (VtxβπΊ)) |
38 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β (VtxβπΊ)) |
39 | | simprr2 1223 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β π β π) |
40 | 39 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β π β π) |
41 | | 4cycl2vnunb 29276 |
. . . . . . . . . . . . . . . . . . 19
β’ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ) β§ π β π)) β Β¬ β!π₯ β (VtxβπΊ){{π, π₯}, {π₯, π}} β (EdgβπΊ)) |
42 | 35, 36, 37, 38, 40, 41 | syl113anc 1383 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β Β¬ β!π₯ β (VtxβπΊ){{π, π₯}, {π₯, π}} β (EdgβπΊ)) |
43 | 42 | pm2.21d 121 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β!π₯ β (VtxβπΊ){{π, π₯}, {π₯, π}} β (EdgβπΊ) β (β―βπΉ) β 4)) |
44 | 43 | com12 32 |
. . . . . . . . . . . . . . . 16
β’
(β!π₯ β
(VtxβπΊ){{π, π₯}, {π₯, π}} β (EdgβπΊ) β ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4)) |
45 | 34, 44 | sylbi 216 |
. . . . . . . . . . . . . . 15
β’
(β!π₯ β
(VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4)) |
46 | 30, 45 | syl6 35 |
. . . . . . . . . . . . . 14
β’ ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (βπ β (VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4))) |
47 | 46 | pm2.43b 55 |
. . . . . . . . . . . . 13
β’
(βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ) β ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4)) |
48 | 47 | adantl 483 |
. . . . . . . . . . . 12
β’ ((πΊ β USGraph β§
βπ β
(VtxβπΊ)βπ β ((VtxβπΊ) β {π})β!π₯ β (VtxβπΊ){{π₯, π}, {π₯, π}} β (EdgβπΊ)) β ((((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4)) |
49 | 7, 48 | sylbi 216 |
. . . . . . . . . . 11
β’ (πΊ β FriendGraph β
((((π β
(VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β§ ((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π)))) β (β―βπΉ) β 4)) |
50 | 49 | expdcom 416 |
. . . . . . . . . 10
β’ (((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β§ (π β (VtxβπΊ) β§ π β (VtxβπΊ))) β (((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β (πΊ β FriendGraph β
(β―βπΉ) β
4))) |
51 | 50 | rexlimdvva 3206 |
. . . . . . . . 9
β’ ((π β (VtxβπΊ) β§ π β (VtxβπΊ)) β (βπ β (VtxβπΊ)βπ β (VtxβπΊ)((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β (πΊ β FriendGraph β
(β―βπΉ) β
4))) |
52 | 51 | rexlimivv 3197 |
. . . . . . . 8
β’
(βπ β
(VtxβπΊ)βπ β (VtxβπΊ)βπ β (VtxβπΊ)βπ β (VtxβπΊ)((({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ)) β§ ({π, π} β (EdgβπΊ) β§ {π, π} β (EdgβπΊ))) β§ ((π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β π))) β (πΊ β FriendGraph β
(β―βπΉ) β
4)) |
53 | 6, 52 | syl 17 |
. . . . . . 7
β’ ((πΊ β UPGraph β§ πΉ(CyclesβπΊ)π β§ (β―βπΉ) = 4) β (πΊ β FriendGraph β
(β―βπΉ) β
4)) |
54 | 53 | 3exp 1120 |
. . . . . 6
β’ (πΊ β UPGraph β (πΉ(CyclesβπΊ)π β ((β―βπΉ) = 4 β (πΊ β FriendGraph β
(β―βπΉ) β
4)))) |
55 | 54 | com34 91 |
. . . . 5
β’ (πΊ β UPGraph β (πΉ(CyclesβπΊ)π β (πΊ β FriendGraph β
((β―βπΉ) = 4
β (β―βπΉ)
β 4)))) |
56 | 55 | com23 86 |
. . . 4
β’ (πΊ β UPGraph β (πΊ β FriendGraph β
(πΉ(CyclesβπΊ)π β ((β―βπΉ) = 4 β (β―βπΉ) β 4)))) |
57 | 3, 56 | mpcom 38 |
. . 3
β’ (πΊ β FriendGraph β
(πΉ(CyclesβπΊ)π β ((β―βπΉ) = 4 β (β―βπΉ) β 4))) |
58 | 57 | imp 408 |
. 2
β’ ((πΊ β FriendGraph β§ πΉ(CyclesβπΊ)π) β ((β―βπΉ) = 4 β (β―βπΉ) β 4)) |
59 | | neqne 2952 |
. 2
β’ (Β¬
(β―βπΉ) = 4
β (β―βπΉ)
β 4) |
60 | 58, 59 | pm2.61d1 180 |
1
β’ ((πΊ β FriendGraph β§ πΉ(CyclesβπΊ)π) β (β―βπΉ) β 4) |