Metamath Proof Explorer

Theorem cusgrm1rusgr

Description: A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for k e. ZZ , then the assumption V =/= (/) could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 26-Dec-2020)

Ref Expression
Hypothesis cusgrrusgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cusgrm1rusgr ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 simpr ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 ∈ ComplUSGraph )
3 1 fusgrvtxfi ⊢ ( 𝐺 ∈ FinUSGraph → 𝑉 ∈ Fin )
4 3 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ∈ Fin )
5 4 adantr ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ∈ Fin )
6 simpr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → 𝑉 ≠ ∅ )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝑉 ≠ ∅ )
8 1 cusgrrusgr ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) )
9 2 5 7 8 syl3anc ⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) ∧ 𝐺 ∈ ComplUSGraph ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) )
10 9 ex ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
11 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
12 1 11 rusgrprop0 ⊢ ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ( 𝐺 ∈ USGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
13 12 simp3d ⊢ ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
14 1 vdiscusgr ⊢ ( 𝐺 ∈ FinUSGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
15 14 adantr ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
16 13 15 syl5 ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝐺 ∈ ComplUSGraph ) )
17 10 16 impbid ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅ ) → ( 𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ) )