Metamath Proof Explorer

Theorem frgrregord013

Description: If a finite friendship graph is K-regular, then it must have order 0, 1 or 3. (Contributed by Alexander van der Vekens, 9-Oct-2018) (Revised by AV, 4-Jun-2021)

Ref Expression
Hypothesis frgrreggt1.v 
|- V = ( Vtx ` G )
Assertion frgrregord013 
|- ( ( G e. FriendGraph /\ V e. Fin /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 hashcl 
 |-  ( V e. Fin -> ( # ` V ) e. NN0 )
3 ax-1 
 |-  ( ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
4 3ioran 
 |-  ( -. ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) <-> ( -. ( # ` V ) = 0 /\ -. ( # ` V ) = 1 /\ -. ( # ` V ) = 3 ) )
5 df-ne 
 |-  ( ( # ` V ) =/= 0 <-> -. ( # ` V ) = 0 )
6 hasheq0 
 |-  ( V e. Fin -> ( ( # ` V ) = 0 <-> V = (/) ) )
7 6 necon3bid 
 |-  ( V e. Fin -> ( ( # ` V ) =/= 0 <-> V =/= (/) ) )
8 7 biimpa 
 |-  ( ( V e. Fin /\ ( # ` V ) =/= 0 ) -> V =/= (/) )
9 elnnne0 
 |-  ( ( # ` V ) e. NN <-> ( ( # ` V ) e. NN0 /\ ( # ` V ) =/= 0 ) )
10 df-ne 
 |-  ( ( # ` V ) =/= 1 <-> -. ( # ` V ) = 1 )
11 eluz2b3 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) <-> ( ( # ` V ) e. NN /\ ( # ` V ) =/= 1 ) )
12 hash2prde 
 |-  ( ( V e. Fin /\ ( # ` V ) = 2 ) -> E. a E. b ( a =/= b /\ V = { a , b } ) )
13 vex 
 |-  a e. _V
14 13 a1i 
 |-  ( a =/= b -> a e. _V )
15 vex 
 |-  b e. _V
16 15 a1i 
 |-  ( a =/= b -> b e. _V )
17 id 
 |-  ( a =/= b -> a =/= b )
18 14 16 17 3jca 
 |-  ( a =/= b -> ( a e. _V /\ b e. _V /\ a =/= b ) )
19 1 eqeq1i 
 |-  ( V = { a , b } <-> ( Vtx ` G ) = { a , b } )
20 19 biimpi 
 |-  ( V = { a , b } -> ( Vtx ` G ) = { a , b } )
21 nfrgr2v 
 |-  ( ( ( a e. _V /\ b e. _V /\ a =/= b ) /\ ( Vtx ` G ) = { a , b } ) -> G e/ FriendGraph )
22 18 20 21 syl2an 
 |-  ( ( a =/= b /\ V = { a , b } ) -> G e/ FriendGraph )
23 df-nel 
 |-  ( G e/ FriendGraph <-> -. G e. FriendGraph )
24 22 23 sylib 
 |-  ( ( a =/= b /\ V = { a , b } ) -> -. G e. FriendGraph )
25 24 pm2.21d 
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
26 25 com23 
 |-  ( ( a =/= b /\ V = { a , b } ) -> ( V =/= (/) -> ( G e. FriendGraph -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
27 26 exlimivv 
 |-  ( E. a E. b ( a =/= b /\ V = { a , b } ) -> ( V =/= (/) -> ( G e. FriendGraph -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
28 12 27 syl 
 |-  ( ( V e. Fin /\ ( # ` V ) = 2 ) -> ( V =/= (/) -> ( G e. FriendGraph -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
29 28 ex 
 |-  ( V e. Fin -> ( ( # ` V ) = 2 -> ( V =/= (/) -> ( G e. FriendGraph -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
30 29 com23 
 |-  ( V e. Fin -> ( V =/= (/) -> ( ( # ` V ) = 2 -> ( G e. FriendGraph -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
31 30 com14 
 |-  ( G e. FriendGraph -> ( V =/= (/) -> ( ( # ` V ) = 2 -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
32 31 a1i 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( ( # ` V ) = 2 -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
33 32 3imp 
 |-  ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph /\ V =/= (/) ) -> ( ( # ` V ) = 2 -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
34 33 com12 
 |-  ( ( # ` V ) = 2 -> ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph /\ V =/= (/) ) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
35 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
36 1 35 rusgrprop0 
 |-  ( G RegUSGraph K -> ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) )
37 eluz2gt1 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> 1 < ( # ` V ) )
38 37 anim1ci 
 |-  ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph ) -> ( G e. FriendGraph /\ 1 < ( # ` V ) ) )
39 1 vdgn0frgrv2 
 |-  ( ( G e. FriendGraph /\ v e. V ) -> ( 1 < ( # ` V ) -> ( ( VtxDeg ` G ) ` v ) =/= 0 ) )
40 39 impancom 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> ( v e. V -> ( ( VtxDeg ` G ) ` v ) =/= 0 ) )
41 40 ralrimiv 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` V ) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 )
42 eqeq2 
 |-  ( K = 0 -> ( ( ( VtxDeg ` G ) ` v ) = K <-> ( ( VtxDeg ` G ) ` v ) = 0 ) )
43 42 ralbidv 
 |-  ( K = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K <-> A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 ) )
44 r19.26 
 |-  ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) = 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 /\ A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 ) )
45 nne 
 |-  ( -. ( ( VtxDeg ` G ) ` v ) =/= 0 <-> ( ( VtxDeg ` G ) ` v ) = 0 )
46 45 bicomi 
 |-  ( ( ( VtxDeg ` G ) ` v ) = 0 <-> -. ( ( VtxDeg ` G ) ` v ) =/= 0 )
47 46 anbi1i 
 |-  ( ( ( ( VtxDeg ` G ) ` v ) = 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> ( -. ( ( VtxDeg ` G ) ` v ) =/= 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) )
48 ancom 
 |-  ( ( -. ( ( VtxDeg ` G ) ` v ) =/= 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> ( ( ( VtxDeg ` G ) ` v ) =/= 0 /\ -. ( ( VtxDeg ` G ) ` v ) =/= 0 ) )
49 pm3.24 
 |-  -. ( ( ( VtxDeg ` G ) ` v ) =/= 0 /\ -. ( ( VtxDeg ` G ) ` v ) =/= 0 )
50 49 bifal 
 |-  ( ( ( ( VtxDeg ` G ) ` v ) =/= 0 /\ -. ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> F. )
51 47 48 50 3bitri 
 |-  ( ( ( ( VtxDeg ` G ) ` v ) = 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> F. )
52 51 ralbii 
 |-  ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) = 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) <-> A. v e. V F. )
53 r19.3rzv 
 |-  ( V =/= (/) -> ( F. <-> A. v e. V F. ) )
54 falim 
 |-  ( F. -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
55 53 54 biimtrrdi 
 |-  ( V =/= (/) -> ( A. v e. V F. -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
56 55 adantl 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( A. v e. V F. -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
57 56 com12 
 |-  ( A. v e. V F. -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
58 52 57 sylbi 
 |-  ( A. v e. V ( ( ( VtxDeg ` G ) ` v ) = 0 /\ ( ( VtxDeg ` G ) ` v ) =/= 0 ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
59 44 58 sylbir 
 |-  ( ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 /\ A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
60 59 ex 
 |-  ( A. v e. V ( ( VtxDeg ` G ) ` v ) = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
61 43 60 biimtrdi 
 |-  ( K = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 -> ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
62 61 com4t 
 |-  ( A. v e. V ( ( VtxDeg ` G ) ` v ) =/= 0 -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
63 38 41 62 3syl 
 |-  ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
64 63 ex 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
65 64 com25 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( G e. FriendGraph -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
66 65 adantl 
 |-  ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( G e. FriendGraph -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
67 66 com15 
 |-  ( G e. FriendGraph -> ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
68 67 com12 
 |-  ( A. v e. V ( ( VtxDeg ` G ) ` v ) = K -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
69 68 3ad2ant3 
 |-  ( ( G e. USGraph /\ K e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = K ) -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
70 36 69 syl 
 |-  ( G RegUSGraph K -> ( G e. FriendGraph -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
71 70 impcom 
 |-  ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( ( V e. Fin /\ V =/= (/) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
72 71 impcom 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
73 1 frrusgrord 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) ) )
74 73 imp 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) )
75 id 
 |-  ( K = 2 -> K = 2 )
76 oveq1 
 |-  ( K = 2 -> ( K - 1 ) = ( 2 - 1 ) )
77 75 76 oveq12d 
 |-  ( K = 2 -> ( K x. ( K - 1 ) ) = ( 2 x. ( 2 - 1 ) ) )
78 77 oveq1d 
 |-  ( K = 2 -> ( ( K x. ( K - 1 ) ) + 1 ) = ( ( 2 x. ( 2 - 1 ) ) + 1 ) )
79 2m1e1 
 |-  ( 2 - 1 ) = 1
80 79 oveq2i 
 |-  ( 2 x. ( 2 - 1 ) ) = ( 2 x. 1 )
81 2t1e2 
 |-  ( 2 x. 1 ) = 2
82 80 81 eqtri 
 |-  ( 2 x. ( 2 - 1 ) ) = 2
83 82 oveq1i 
 |-  ( ( 2 x. ( 2 - 1 ) ) + 1 ) = ( 2 + 1 )
84 2p1e3 
 |-  ( 2 + 1 ) = 3
85 83 84 eqtri 
 |-  ( ( 2 x. ( 2 - 1 ) ) + 1 ) = 3
86 78 85 eqtrdi 
 |-  ( K = 2 -> ( ( K x. ( K - 1 ) ) + 1 ) = 3 )
87 86 eqeq2d 
 |-  ( K = 2 -> ( ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) <-> ( # ` V ) = 3 ) )
88 pm2.21 
 |-  ( -. ( # ` V ) = 3 -> ( ( # ` V ) = 3 -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
89 88 ad2antrr 
 |-  ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 3 -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
90 89 com12 
 |-  ( ( # ` V ) = 3 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
91 87 90 biimtrdi 
 |-  ( K = 2 -> ( ( # ` V ) = ( ( K x. ( K - 1 ) ) + 1 ) -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
92 74 91 syl5com 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 2 -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
93 1 frgrreg 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( ( G e. FriendGraph /\ G RegUSGraph K ) -> ( K = 0 \/ K = 2 ) ) )
94 93 imp 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( K = 0 \/ K = 2 ) )
95 72 92 94 mpjaod 
 |-  ( ( ( V e. Fin /\ V =/= (/) ) /\ ( G e. FriendGraph /\ G RegUSGraph K ) ) -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
96 95 exp32 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
97 96 com34 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( G e. FriendGraph -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
98 97 com23 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( ( ( -. ( # ` V ) = 3 /\ -. ( # ` V ) = 2 ) /\ ( # ` V ) e. ( ZZ>= ` 2 ) ) -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
99 98 exp4c 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( -. ( # ` V ) = 3 -> ( -. ( # ` V ) = 2 -> ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
100 99 com34 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( -. ( # ` V ) = 3 -> ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( -. ( # ` V ) = 2 -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
101 100 com25 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( G e. FriendGraph -> ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( -. ( # ` V ) = 2 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
102 101 ex 
 |-  ( V e. Fin -> ( V =/= (/) -> ( G e. FriendGraph -> ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( -. ( # ` V ) = 2 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
103 102 com23 
 |-  ( V e. Fin -> ( G e. FriendGraph -> ( V =/= (/) -> ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( -. ( # ` V ) = 2 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
104 103 com14 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. ( # ` V ) = 2 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
105 104 3imp 
 |-  ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph /\ V =/= (/) ) -> ( V e. Fin -> ( -. ( # ` V ) = 2 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
106 105 com3r 
 |-  ( -. ( # ` V ) = 2 -> ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph /\ V =/= (/) ) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
107 34 106 pm2.61i 
 |-  ( ( ( # ` V ) e. ( ZZ>= ` 2 ) /\ G e. FriendGraph /\ V =/= (/) ) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
108 107 3exp 
 |-  ( ( # ` V ) e. ( ZZ>= ` 2 ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
109 11 108 sylbir 
 |-  ( ( ( # ` V ) e. NN /\ ( # ` V ) =/= 1 ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
110 109 ex 
 |-  ( ( # ` V ) e. NN -> ( ( # ` V ) =/= 1 -> ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
111 10 110 biimtrrid 
 |-  ( ( # ` V ) e. NN -> ( -. ( # ` V ) = 1 -> ( G e. FriendGraph -> ( V =/= (/) -> ( V e. Fin -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
112 111 com25 
 |-  ( ( # ` V ) e. NN -> ( V e. Fin -> ( G e. FriendGraph -> ( V =/= (/) -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
113 9 112 sylbir 
 |-  ( ( ( # ` V ) e. NN0 /\ ( # ` V ) =/= 0 ) -> ( V e. Fin -> ( G e. FriendGraph -> ( V =/= (/) -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
114 113 ex 
 |-  ( ( # ` V ) e. NN0 -> ( ( # ` V ) =/= 0 -> ( V e. Fin -> ( G e. FriendGraph -> ( V =/= (/) -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) ) )
115 114 impcomd 
 |-  ( ( # ` V ) e. NN0 -> ( ( V e. Fin /\ ( # ` V ) =/= 0 ) -> ( G e. FriendGraph -> ( V =/= (/) -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
116 115 com14 
 |-  ( V =/= (/) -> ( ( V e. Fin /\ ( # ` V ) =/= 0 ) -> ( G e. FriendGraph -> ( ( # ` V ) e. NN0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
117 8 116 mpcom 
 |-  ( ( V e. Fin /\ ( # ` V ) =/= 0 ) -> ( G e. FriendGraph -> ( ( # ` V ) e. NN0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) )
118 117 ex 
 |-  ( V e. Fin -> ( ( # ` V ) =/= 0 -> ( G e. FriendGraph -> ( ( # ` V ) e. NN0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
119 118 com14 
 |-  ( ( # ` V ) e. NN0 -> ( ( # ` V ) =/= 0 -> ( G e. FriendGraph -> ( V e. Fin -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
120 5 119 biimtrrid 
 |-  ( ( # ` V ) e. NN0 -> ( -. ( # ` V ) = 0 -> ( G e. FriendGraph -> ( V e. Fin -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
121 120 com24 
 |-  ( ( # ` V ) e. NN0 -> ( V e. Fin -> ( G e. FriendGraph -> ( -. ( # ` V ) = 0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) ) ) )
122 121 3imp 
 |-  ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) -> ( -. ( # ` V ) = 0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
123 122 com25 
 |-  ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) -> ( G RegUSGraph K -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( -. ( # ` V ) = 0 -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) ) )
124 123 imp 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( -. ( # ` V ) = 0 -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
125 124 com14 
 |-  ( -. ( # ` V ) = 0 -> ( -. ( # ` V ) = 1 -> ( -. ( # ` V ) = 3 -> ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
126 125 3imp 
 |-  ( ( -. ( # ` V ) = 0 /\ -. ( # ` V ) = 1 /\ -. ( # ` V ) = 3 ) -> ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
127 4 126 sylbi 
 |-  ( -. ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
128 3 127 pm2.61i 
 |-  ( ( ( ( # ` V ) e. NN0 /\ V e. Fin /\ G e. FriendGraph ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
129 128 3exp1 
 |-  ( ( # ` V ) e. NN0 -> ( V e. Fin -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
130 2 129 mpcom 
 |-  ( V e. Fin -> ( G e. FriendGraph -> ( G RegUSGraph K -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
131 130 3imp21 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )