Step | Hyp | Ref
| Expression |
1 | | ancom 462 |
. . . . . . . . 9
β’ ((π β Fin β§ π β β
) β (π β β
β§ π β Fin)) |
2 | | ancom 462 |
. . . . . . . . 9
β’ ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph )) |
3 | 1, 2 | anbi12i 628 |
. . . . . . . 8
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β ((π β β
β§ π β Fin) β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ))) |
4 | 3 | biimpi 215 |
. . . . . . 7
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β ((π β β
β§ π β Fin) β§ (πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ))) |
5 | 4 | ancomd 463 |
. . . . . 6
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β ((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β β
β§ π β Fin))) |
6 | | frgrreggt1.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
7 | 6 | numclwwlk7lem 29375 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ πΊ β FriendGraph ) β§ (π β β
β§ π β Fin)) β πΎ β
β0) |
8 | 5, 7 | syl 17 |
. . . . 5
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β πΎ β
β0) |
9 | | neanior 3038 |
. . . . . . . 8
β’ ((πΎ β 0 β§ πΎ β 2) β Β¬ (πΎ = 0 β¨ πΎ = 2)) |
10 | | nn0re 12429 |
. . . . . . . . . . . . . 14
β’ (πΎ β β0
β πΎ β
β) |
11 | | 1re 11162 |
. . . . . . . . . . . . . 14
β’ 1 β
β |
12 | | lenlt 11240 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β β§ 1 β
β) β (πΎ β€ 1
β Β¬ 1 < πΎ)) |
13 | 10, 11, 12 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (πΎ β β0
β (πΎ β€ 1 β
Β¬ 1 < πΎ)) |
14 | 13 | adantl 483 |
. . . . . . . . . . . 12
β’ (((πΎ β 0 β§ πΎ β 2) β§ πΎ β β0) β (πΎ β€ 1 β Β¬ 1 <
πΎ)) |
15 | | elnnne0 12434 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β β β (πΎ β β0
β§ πΎ β
0)) |
16 | | nnle1eq1 12190 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β β β (πΎ β€ 1 β πΎ = 1)) |
17 | 16 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β β β (πΎ β€ 1 β πΎ = 1)) |
18 | 15, 17 | sylbir 234 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β β0
β§ πΎ β 0) β
(πΎ β€ 1 β πΎ = 1)) |
19 | 18 | a1d 25 |
. . . . . . . . . . . . . 14
β’ ((πΎ β β0
β§ πΎ β 0) β
(πΎ β 2 β (πΎ β€ 1 β πΎ = 1))) |
20 | 19 | expimpd 455 |
. . . . . . . . . . . . 13
β’ (πΎ β β0
β ((πΎ β 0 β§
πΎ β 2) β (πΎ β€ 1 β πΎ = 1))) |
21 | 20 | impcom 409 |
. . . . . . . . . . . 12
β’ (((πΎ β 0 β§ πΎ β 2) β§ πΎ β β0) β (πΎ β€ 1 β πΎ = 1)) |
22 | 14, 21 | sylbird 260 |
. . . . . . . . . . 11
β’ (((πΎ β 0 β§ πΎ β 2) β§ πΎ β β0) β (Β¬ 1
< πΎ β πΎ = 1)) |
23 | 6 | fveq2i 6850 |
. . . . . . . . . . . . . . . . . 18
β’
(β―βπ) =
(β―β(VtxβπΊ)) |
24 | 23 | eqeq1i 2742 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ) =
1 β (β―β(VtxβπΊ)) = 1) |
25 | 24 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
1 β (β―β(VtxβπΊ)) = 1) |
26 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β πΊ RegUSGraph πΎ) |
27 | 26 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β πΊ RegUSGraph πΎ) |
28 | | rusgr1vtx 28578 |
. . . . . . . . . . . . . . . 16
β’
(((β―β(VtxβπΊ)) = 1 β§ πΊ RegUSGraph πΎ) β πΎ = 0) |
29 | 25, 27, 28 | syl2an 597 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ)
= 1 β§ ((π β Fin
β§ π β β
) β§
(πΊ β FriendGraph β§
πΊ RegUSGraph πΎ))) β πΎ = 0) |
30 | 29 | orcd 872 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
= 1 β§ ((π β Fin
β§ π β β
) β§
(πΊ β FriendGraph β§
πΊ RegUSGraph πΎ))) β (πΎ = 0 β¨ πΎ = 2)) |
31 | 30 | ex 414 |
. . . . . . . . . . . . 13
β’
((β―βπ) =
1 β (((π β Fin
β§ π β β
) β§
(πΊ β FriendGraph β§
πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))) |
32 | 31 | a1d 25 |
. . . . . . . . . . . 12
β’
((β―βπ) =
1 β (πΎ = 1 β
(((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)))) |
33 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
34 | 6, 33 | rusgrprop0 28557 |
. . . . . . . . . . . . . . . 16
β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0*
β§ βπ£ β
π ((VtxDegβπΊ)βπ£) = πΎ)) |
35 | | simp2 1138 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Β¬
(β―βπ) = 1 β§
πΊ β FriendGraph β§
(π β Fin β§ π β β
)) β πΊ β FriendGraph
) |
36 | | hashnncl 14273 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
37 | | df-ne 2945 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ)
β 1 β Β¬ (β―βπ) = 1) |
38 | | nngt1ne1 12189 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β β (1 < (β―βπ) β (β―βπ) β 1)) |
39 | 38 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ)
β β β ((β―βπ) β 1 β 1 < (β―βπ))) |
40 | 37, 39 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ)
β β β (Β¬ (β―βπ) = 1 β 1 < (β―βπ))) |
41 | 36, 40 | syl6bir 254 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β Fin β (π β β
β (Β¬
(β―βπ) = 1
β 1 < (β―βπ)))) |
42 | 41 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Fin β§ π β β
) β (Β¬
(β―βπ) = 1
β 1 < (β―βπ))) |
43 | 42 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((Β¬
(β―βπ) = 1 β§
(π β Fin β§ π β β
)) β 1 <
(β―βπ)) |
44 | 6 | vdgn1frgrv3 29283 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΊ β FriendGraph β§ 1 <
(β―βπ)) β
βπ£ β π ((VtxDegβπΊ)βπ£) β 1) |
45 | 35, 43, 44 | 3imp3i2an 1346 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
(β―βπ) = 1 β§
πΊ β FriendGraph β§
(π β Fin β§ π β β
)) β
βπ£ β π ((VtxDegβπΊ)βπ£) β 1) |
46 | | r19.26 3115 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ) β (βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β§ βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ)) |
47 | | r19.2z 4457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β β
β§
βπ£ β π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ)) β βπ£ β π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ)) |
48 | | neeq1 3007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((VtxDegβπΊ)βπ£) = πΎ β (((VtxDegβπΊ)βπ£) β 1 β πΎ β 1)) |
49 | 48 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((VtxDegβπΊ)βπ£) = πΎ β (((VtxDegβπΊ)βπ£) β 1 β πΎ β 1)) |
50 | 49 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ) β πΎ β 1) |
51 | | eqneqall 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (πΎ = 1 β (πΎ β 1 β (πΎ = 0 β¨ πΎ = 2))) |
52 | 51 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (πΎ β 1 β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2))) |
53 | 50, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2))) |
54 | 53 | rexlimivw 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ£ β
π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2))) |
55 | 47, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β β
β§
βπ£ β π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ)) β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2))) |
56 | 55 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β
β
(βπ£ β π (((VtxDegβπΊ)βπ£) β 1 β§ ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2)))) |
57 | 46, 56 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β
β
((βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β§ βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2)))) |
58 | 57 | expd 417 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β
β
(βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 1 β (πΎ = 0 β¨ πΎ = 2))))) |
59 | 58 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β
β
(βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β (πΎ = 1 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 0 β¨ πΎ = 2))))) |
60 | 59 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β Fin β§ π β β
) β
(βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β (πΎ = 1 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 0 β¨ πΎ = 2))))) |
61 | 60 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Β¬
(β―βπ) = 1 β§
πΊ β FriendGraph β§
(π β Fin β§ π β β
)) β
(βπ£ β π ((VtxDegβπΊ)βπ£) β 1 β (πΎ = 1 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 0 β¨ πΎ = 2))))) |
62 | 45, 61 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Β¬
(β―βπ) = 1 β§
πΊ β FriendGraph β§
(π β Fin β§ π β β
)) β (πΎ = 1 β (βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 0 β¨ πΎ = 2)))) |
63 | 62 | 3exp 1120 |
. . . . . . . . . . . . . . . . . 18
β’ (Β¬
(β―βπ) = 1
β (πΊ β
FriendGraph β ((π
β Fin β§ π β
β
) β (πΎ = 1
β (βπ£ β
π ((VtxDegβπΊ)βπ£) = πΎ β (πΎ = 0 β¨ πΎ = 2)))))) |
64 | 63 | com15 101 |
. . . . . . . . . . . . . . . . 17
β’
(βπ£ β
π ((VtxDegβπΊ)βπ£) = πΎ β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 1 β (Β¬
(β―βπ) = 1
β (πΎ = 0 β¨ πΎ = 2)))))) |
65 | 64 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ β USGraph β§ πΎ β
β0* β§ βπ£ β π ((VtxDegβπΊ)βπ£) = πΎ) β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 1 β (Β¬
(β―βπ) = 1
β (πΎ = 0 β¨ πΎ = 2)))))) |
66 | 34, 65 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (πΊ RegUSGraph πΎ β (πΊ β FriendGraph β ((π β Fin β§ π β β
) β (πΎ = 1 β (Β¬
(β―βπ) = 1
β (πΎ = 0 β¨ πΎ = 2)))))) |
67 | 66 | impcom 409 |
. . . . . . . . . . . . . 14
β’ ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β ((π β Fin β§ π β β
) β (πΎ = 1 β (Β¬ (β―βπ) = 1 β (πΎ = 0 β¨ πΎ = 2))))) |
68 | 67 | impcom 409 |
. . . . . . . . . . . . 13
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 1 β (Β¬ (β―βπ) = 1 β (πΎ = 0 β¨ πΎ = 2)))) |
69 | 68 | com13 88 |
. . . . . . . . . . . 12
β’ (Β¬
(β―βπ) = 1
β (πΎ = 1 β
(((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)))) |
70 | 32, 69 | pm2.61i 182 |
. . . . . . . . . . 11
β’ (πΎ = 1 β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))) |
71 | 22, 70 | syl6 35 |
. . . . . . . . . 10
β’ (((πΎ β 0 β§ πΎ β 2) β§ πΎ β β0) β (Β¬ 1
< πΎ β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)))) |
72 | 71 | ex 414 |
. . . . . . . . 9
β’ ((πΎ β 0 β§ πΎ β 2) β (πΎ β β0 β (Β¬ 1
< πΎ β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))))) |
73 | 72 | com23 86 |
. . . . . . . 8
β’ ((πΎ β 0 β§ πΎ β 2) β (Β¬ 1 < πΎ β (πΎ β β0 β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))))) |
74 | 9, 73 | sylbir 234 |
. . . . . . 7
β’ (Β¬
(πΎ = 0 β¨ πΎ = 2) β (Β¬ 1 < πΎ β (πΎ β β0 β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))))) |
75 | 74 | impcom 409 |
. . . . . 6
β’ ((Β¬ 1
< πΎ β§ Β¬ (πΎ = 0 β¨ πΎ = 2)) β (πΎ β β0 β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)))) |
76 | 75 | com13 88 |
. . . . 5
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ β β0 β ((Β¬ 1
< πΎ β§ Β¬ (πΎ = 0 β¨ πΎ = 2)) β (πΎ = 0 β¨ πΎ = 2)))) |
77 | 8, 76 | mpd 15 |
. . . 4
β’ (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β ((Β¬ 1 < πΎ β§ Β¬ (πΎ = 0 β¨ πΎ = 2)) β (πΎ = 0 β¨ πΎ = 2))) |
78 | 77 | com12 32 |
. . 3
β’ ((Β¬ 1
< πΎ β§ Β¬ (πΎ = 0 β¨ πΎ = 2)) β (((π β Fin β§ π β β
) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2))) |
79 | 78 | exp4b 432 |
. 2
β’ (Β¬ 1
< πΎ β (Β¬ (πΎ = 0 β¨ πΎ = 2) β ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΎ = 0 β¨ πΎ = 2))))) |
80 | | simprl 770 |
. . . . 5
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β πΊ β FriendGraph ) |
81 | | simpl 484 |
. . . . . 6
β’ ((π β Fin β§ π β β
) β π β Fin) |
82 | 81 | ad2antlr 726 |
. . . . 5
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β π β Fin) |
83 | | simpr 486 |
. . . . . 6
β’ ((π β Fin β§ π β β
) β π β β
) |
84 | 83 | ad2antlr 726 |
. . . . 5
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β π β β
) |
85 | | simpl 484 |
. . . . . 6
β’ ((1 <
πΎ β§ (π β Fin β§ π β β
)) β 1 < πΎ) |
86 | 85, 26 | anim12ci 615 |
. . . . 5
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΊ RegUSGraph πΎ β§ 1 < πΎ)) |
87 | 6 | frgrreggt1 29379 |
. . . . . 6
β’ ((πΊ β FriendGraph β§ π β Fin β§ π β β
) β ((πΊ RegUSGraph πΎ β§ 1 < πΎ) β πΎ = 2)) |
88 | 87 | imp 408 |
. . . . 5
β’ (((πΊ β FriendGraph β§ π β Fin β§ π β β
) β§ (πΊ RegUSGraph πΎ β§ 1 < πΎ)) β πΎ = 2) |
89 | 80, 82, 84, 86, 88 | syl31anc 1374 |
. . . 4
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β πΎ = 2) |
90 | 89 | olcd 873 |
. . 3
β’ (((1 <
πΎ β§ (π β Fin β§ π β β
)) β§ (πΊ β FriendGraph β§ πΊ RegUSGraph πΎ)) β (πΎ = 0 β¨ πΎ = 2)) |
91 | 90 | exp31 421 |
. 2
β’ (1 <
πΎ β ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΎ = 0 β¨ πΎ = 2)))) |
92 | | 2a1 28 |
. 2
β’ ((πΎ = 0 β¨ πΎ = 2) β ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΎ = 0 β¨ πΎ = 2)))) |
93 | 79, 91, 92 | pm2.61ii 183 |
1
β’ ((π β Fin β§ π β β
) β ((πΊ β FriendGraph β§ πΊ RegUSGraph πΎ) β (πΎ = 0 β¨ πΎ = 2))) |