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 e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G RegUSGraph ( ( # ` V ) - 1 ) )

Proof

Step Hyp Ref Expression
1 cusgrrusgr.v 
 |-  V = ( Vtx ` G )
2 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
3 2 3ad2ant1 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G e. USGraph )
4 hashnncl 
 |-  ( V e. Fin -> ( ( # ` V ) e. NN <-> V =/= (/) ) )
5 nnm1nn0 
 |-  ( ( # ` V ) e. NN -> ( ( # ` V ) - 1 ) e. NN0 )
6 5 nn0xnn0d 
 |-  ( ( # ` V ) e. NN -> ( ( # ` V ) - 1 ) e. NN0* )
7 4 6 syl6bir 
 |-  ( V e. Fin -> ( V =/= (/) -> ( ( # ` V ) - 1 ) e. NN0* ) )
8 7 imp 
 |-  ( ( V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) - 1 ) e. NN0* )
9 8 3adant1 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> ( ( # ` V ) - 1 ) e. NN0* )
10 cusgrcplgr 
 |-  ( G e. ComplUSGraph -> G e. ComplGraph )
11 10 3ad2ant1 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G e. ComplGraph )
12 1 nbcplgr 
 |-  ( ( G e. ComplGraph /\ v e. V ) -> ( G NeighbVtx v ) = ( V \ { v } ) )
13 11 12 sylan 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) -> ( G NeighbVtx v ) = ( V \ { v } ) )
14 13 ralrimiva 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> A. v e. V ( G NeighbVtx v ) = ( V \ { v } ) )
15 3 anim1i 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) -> ( G e. USGraph /\ v e. V ) )
16 15 adantr 
 |-  ( ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) /\ ( G NeighbVtx v ) = ( V \ { v } ) ) -> ( G e. USGraph /\ v e. V ) )
17 1 hashnbusgrvd 
 |-  ( ( G e. USGraph /\ v e. V ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
18 16 17 syl 
 |-  ( ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) /\ ( G NeighbVtx v ) = ( V \ { v } ) ) -> ( # ` ( G NeighbVtx v ) ) = ( ( VtxDeg ` G ) ` v ) )
19 fveq2 
 |-  ( ( G NeighbVtx v ) = ( V \ { v } ) -> ( # ` ( G NeighbVtx v ) ) = ( # ` ( V \ { v } ) ) )
20 hashdifsn 
 |-  ( ( V e. Fin /\ v e. V ) -> ( # ` ( V \ { v } ) ) = ( ( # ` V ) - 1 ) )
21 20 3ad2antl2 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) -> ( # ` ( V \ { v } ) ) = ( ( # ` V ) - 1 ) )
22 19 21 sylan9eqr 
 |-  ( ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) /\ ( G NeighbVtx v ) = ( V \ { v } ) ) -> ( # ` ( G NeighbVtx v ) ) = ( ( # ` V ) - 1 ) )
23 18 22 eqtr3d 
 |-  ( ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) /\ ( G NeighbVtx v ) = ( V \ { v } ) ) -> ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) )
24 23 ex 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) /\ v e. V ) -> ( ( G NeighbVtx v ) = ( V \ { v } ) -> ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )
25 24 ralimdva 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( G NeighbVtx v ) = ( V \ { v } ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) )
26 14 25 mpd 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) )
27 simp1 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G e. ComplUSGraph )
28 ovex 
 |-  ( ( # ` V ) - 1 ) e. _V
29 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
30 1 29 isrusgr0 
 |-  ( ( G e. ComplUSGraph /\ ( ( # ` V ) - 1 ) e. _V ) -> ( G RegUSGraph ( ( # ` V ) - 1 ) <-> ( G e. USGraph /\ ( ( # ` V ) - 1 ) e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) ) )
31 27 28 30 sylancl 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> ( G RegUSGraph ( ( # ` V ) - 1 ) <-> ( G e. USGraph /\ ( ( # ` V ) - 1 ) e. NN0* /\ A. v e. V ( ( VtxDeg ` G ) ` v ) = ( ( # ` V ) - 1 ) ) ) )
32 3 9 26 31 mpbir3and 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ V =/= (/) ) -> G RegUSGraph ( ( # ` V ) - 1 ) )