Metamath Proof Explorer

Theorem frgrregord13

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

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

Proof

Step Hyp Ref Expression
1 frgrreggt1.v 
 |-  V = ( Vtx ` G )
2 simpl1 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> G e. FriendGraph )
3 simpl2 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> V e. Fin )
4 simpr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> G RegUSGraph K )
5 1 frgrregord013 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
6 2 3 4 5 syl3anc 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
7 hasheq0 
 |-  ( V e. Fin -> ( ( # ` V ) = 0 <-> V = (/) ) )
8 eqneqall 
 |-  ( V = (/) -> ( V =/= (/) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
9 7 8 syl6bi 
 |-  ( V e. Fin -> ( ( # ` V ) = 0 -> ( V =/= (/) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
10 9 com23 
 |-  ( V e. Fin -> ( V =/= (/) -> ( ( # ` V ) = 0 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) )
11 10 a1i 
 |-  ( G e. FriendGraph -> ( V e. Fin -> ( V =/= (/) -> ( ( # ` V ) = 0 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) ) ) )
12 11 3imp 
 |-  ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) = 0 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
13 12 adantr 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 0 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
14 13 com12 
 |-  ( ( # ` V ) = 0 -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
15 orc 
 |-  ( ( # ` V ) = 1 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
16 15 a1d 
 |-  ( ( # ` V ) = 1 -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
17 olc 
 |-  ( ( # ` V ) = 3 -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )
18 17 a1d 
 |-  ( ( # ` V ) = 3 -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
19 14 16 18 3jaoi 
 |-  ( ( ( # ` V ) = 0 \/ ( # ` V ) = 1 \/ ( # ` V ) = 3 ) -> ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) ) )
20 6 19 mpcom 
 |-  ( ( ( G e. FriendGraph /\ V e. Fin /\ V =/= (/) ) /\ G RegUSGraph K ) -> ( ( # ` V ) = 1 \/ ( # ` V ) = 3 ) )