Metamath Proof Explorer

Theorem numclwwlk7lem

Description: Lemma for numclwwlk7 , frgrreggt1 and frgrreg : If a finite, nonempty friendship graph is K-regular, the K is a nonnegative integer. (Contributed by AV, 3-Jun-2021)

Ref Expression
Hypothesis numclwwlk7lem.v 
|- V = ( Vtx ` G )
Assertion numclwwlk7lem 
|- ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> K e. NN0 )

Proof

Step Hyp Ref Expression
1 numclwwlk7lem.v 
 |-  V = ( Vtx ` G )
2 1 finrusgrfusgr 
 |-  ( ( G RegUSGraph K /\ V e. Fin ) -> G e. FinUSGraph )
3 2 ad2ant2rl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> G e. FinUSGraph )
4 simpll 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> G RegUSGraph K )
5 simprl 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> V =/= (/) )
6 1 frusgrnn0 
 |-  ( ( G e. FinUSGraph /\ G RegUSGraph K /\ V =/= (/) ) -> K e. NN0 )
7 3 4 5 6 syl3anc 
 |-  ( ( ( G RegUSGraph K /\ G e. FriendGraph ) /\ ( V =/= (/) /\ V e. Fin ) ) -> K e. NN0 )