Step | Hyp | Ref
| Expression |
1 | | frgrwopreg.v |
. . 3
Vtx |
2 | | frgrwopreg.d |
. . 3
VtxDeg |
3 | | frgrwopreg.a |
. . 3
|
4 | | frgrwopreg.b |
. . 3
|
5 | 1, 2, 3, 4 | frgrwopreglem1 27176 |
. 2
|
6 | | hashv01gt1 13133 |
. . . 4
|
7 | | hasheq0 13154 |
. . . . . 6
|
8 | | biidd 252 |
. . . . . 6
|
9 | | biidd 252 |
. . . . . 6
|
10 | 7, 8, 9 | 3orbi123d 1398 |
. . . . 5
|
11 | | hashv01gt1 13133 |
. . . . . . 7
|
12 | | hasheq0 13154 |
. . . . . . . . 9
|
13 | | biidd 252 |
. . . . . . . . 9
|
14 | | biidd 252 |
. . . . . . . . 9
|
15 | 12, 13, 14 | 3orbi123d 1398 |
. . . . . . . 8
|
16 | | olc 399 |
. . . . . . . . . . 11
|
17 | 16 | olcd 408 |
. . . . . . . . . 10
|
18 | 17 | 2a1d 26 |
. . . . . . . . 9
FriendGraph
|
19 | | orc 400 |
. . . . . . . . . . 11
|
20 | 19 | olcd 408 |
. . . . . . . . . 10
|
21 | 20 | 2a1d 26 |
. . . . . . . . 9
FriendGraph |
22 | | olc 399 |
. . . . . . . . . . . . 13
|
23 | 22 | orcd 407 |
. . . . . . . . . . . 12
|
24 | 23 | 2a1d 26 |
. . . . . . . . . . 11
FriendGraph
|
25 | | orc 400 |
. . . . . . . . . . . . 13
|
26 | 25 | orcd 407 |
. . . . . . . . . . . 12
|
27 | 26 | 2a1d 26 |
. . . . . . . . . . 11
FriendGraph
|
28 | | eqid 2622 |
. . . . . . . . . . . . . . 15
Edg Edg |
29 | 1, 2, 3, 4, 28 | frgrwopreglem5 27185 |
. . . . . . . . . . . . . 14
FriendGraph
Edg Edg
Edg
Edg |
30 | | frgrusgr 27124 |
. . . . . . . . . . . . . . . 16
FriendGraph USGraph |
31 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
USGraph |
32 | | elrabi 3359 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
33 | 32, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
34 | 33 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
35 | 34 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
36 | | rabidim1 3117 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
37 | 36, 3 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
39 | 38 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
40 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
41 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
42 | 41, 4 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
43 | 42 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
44 | 43 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
45 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
46 | 45, 4 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
47 | 46 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
48 | 47 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
49 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
|
50 | 1, 28 | 4cyclusnfrgr 27156 |
. . . . . . . . . . . . . . . . . . . . . . 23
USGraph
Edg Edg
Edg
Edg
FriendGraph |
51 | 31, 35, 39, 40, 44, 48, 49, 50 | syl133anc 1349 |
. . . . . . . . . . . . . . . . . . . . . 22
USGraph
Edg
Edg Edg Edg FriendGraph |
52 | 51 | exp4b 632 |
. . . . . . . . . . . . . . . . . . . . 21
USGraph
Edg Edg
Edg Edg FriendGraph |
53 | 52 | 3impd 1281 |
. . . . . . . . . . . . . . . . . . . 20
USGraph
Edg Edg
Edg
Edg
FriendGraph |
54 | | df-nel 2898 |
. . . . . . . . . . . . . . . . . . . . 21
FriendGraph FriendGraph |
55 | | pm2.21 120 |
. . . . . . . . . . . . . . . . . . . . 21
FriendGraph
FriendGraph
|
56 | 54, 55 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . 20
FriendGraph FriendGraph
|
57 | 53, 56 | syl6 35 |
. . . . . . . . . . . . . . . . . . 19
USGraph
Edg Edg
Edg
Edg
FriendGraph
|
58 | 57 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . . 18
USGraph
Edg
Edg Edg Edg FriendGraph |
59 | 58 | rexlimdvva 3038 |
. . . . . . . . . . . . . . . . 17
USGraph
Edg Edg
Edg
Edg
FriendGraph
|
60 | 59 | com23 86 |
. . . . . . . . . . . . . . . 16
USGraph FriendGraph Edg Edg
Edg
Edg
|
61 | 30, 60 | mpcom 38 |
. . . . . . . . . . . . . . 15
FriendGraph
Edg Edg
Edg
Edg
|
62 | 61 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
FriendGraph
Edg Edg
Edg
Edg
|
63 | 29, 62 | mpd 15 |
. . . . . . . . . . . . 13
FriendGraph |
64 | 63 | 3exp 1264 |
. . . . . . . . . . . 12
FriendGraph |
65 | 64 | com3l 89 |
. . . . . . . . . . 11
FriendGraph
|
66 | 24, 27, 65 | 3jaoi 1391 |
. . . . . . . . . 10
FriendGraph
|
67 | 66 | com12 32 |
. . . . . . . . 9
FriendGraph
|
68 | 18, 21, 67 | 3jaoi 1391 |
. . . . . . . 8
FriendGraph
|
69 | 15, 68 | syl6bi 243 |
. . . . . . 7
FriendGraph |
70 | 11, 69 | mpd 15 |
. . . . . 6
FriendGraph |
71 | 70 | com12 32 |
. . . . 5
FriendGraph
|
72 | 10, 71 | syl6bi 243 |
. . . 4
FriendGraph |
73 | 6, 72 | mpd 15 |
. . 3
FriendGraph
|
74 | 73 | imp 445 |
. 2
FriendGraph |
75 | 5, 74 | ax-mp 5 |
1
FriendGraph |