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 ⊢V=Vtx⁡G
Assertion cusgrrusgr ⊢G∈ComplUSGraph∧V∈Fin∧V≠∅→GRegUSGraphV−1

Proof

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