Metamath Proof Explorer

Theorem cusgrrusgr

Description: A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018) (Revised by AV, 26-Dec-2020)

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

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrusgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )
3 2 3ad2ant1 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 ∈ USGraph )
4 hashnncl ⊢ ( 𝑉 ∈ Fin → ( ( ♯ ‘ 𝑉 ) ∈ ℕ ↔ 𝑉 ≠ ∅ ) )
5 nnm1nn0 ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0 )
6 5 nn0xnn0d ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* )
7 4 6 syl6bir ⊢ ( 𝑉 ∈ Fin → ( 𝑉 ≠ ∅ → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ) )
8 7 imp ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* )
9 8 3adant1 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* )
10 cusgrcplgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ ComplGraph )
11 10 3ad2ant1 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 ∈ ComplGraph )
12 1 nbcplgr ⊢ ( ( 𝐺 ∈ ComplGraph ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) )
13 11 12 sylan ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) )
14 13 ralrimiva ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ∀ 𝑣 ∈ 𝑉 ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) )
15 3 anim1i ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) )
16 15 adantr ⊢ ( ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) )
17 1 hashnbusgrvd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
18 16 17 syl ⊢ ( ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) )
19 fveq2 ⊢ ( ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ♯ ‘ ( 𝑉 ∖ { 𝑣 } ) ) )
20 hashdifsn ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑣 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
21 20 3ad2antl2 ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∖ { 𝑣 } ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
22 19 21 sylan9eqr ⊢ ( ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑣 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
23 18 22 eqtr3d ⊢ ( ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) ∧ ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
24 23 ex ⊢ ( ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
25 24 ralimdva ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑣 ∈ 𝑉 ( 𝐺 NeighbVtx 𝑣 ) = ( 𝑉 ∖ { 𝑣 } ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) )
26 14 25 mpd ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) )
27 simp1 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 ∈ ComplUSGraph )
28 ovex ⊢ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ V
29 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
30 1 29 isrusgr0 ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ V ) → ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ↔ ( 𝐺 ∈ USGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) )
31 27 28 30 sylancl ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → ( 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) ↔ ( 𝐺 ∈ USGraph ∧ ( ( ♯ ‘ 𝑉 ) − 1 ) ∈ ℕ0* ∧ ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) ) )
32 3 9 26 31 mpbir3and ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅ ) → 𝐺 RegUSGraph ( ( ♯ ‘ 𝑉 ) − 1 ) )