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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	numclwwlk7lem	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		numclwwlk7lem.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2	1	finrusgrfusgr	⊢ ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin ) → 𝐺 ∈ FinUSGraph )
3	2	ad2ant2rl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 ∈ FinUSGraph )
4		simpll	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐺 RegUSGraph 𝐾 )
5		simprl	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝑉 ≠ ∅ )
6	1	frusgrnn0	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅ ) → 𝐾 ∈ ℕ0 )
7	3 4 5 6	syl3anc	⊢ ( ( ( 𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ ( 𝑉 ≠ ∅ ∧ 𝑉 ∈ Fin ) ) → 𝐾 ∈ ℕ0 )