Metamath Proof Explorer

Theorem cusgrsize

Description: The size of a finite complete simple graph with n vertices ( n e. NN0 ) is ( n _C 2 ) (" n choose 2") resp. ( ( ( n - 1 ) * n ) / 2 ) , see definition in section I.1 of Bollobas p. 3 . (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 10-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v 
|- V = ( Vtx ` G )
cusgrsizeindb0.e 
|- E = ( Edg ` G )
Assertion cusgrsize 
|- ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v 
 |-  V = ( Vtx ` G )
2 cusgrsizeindb0.e 
 |-  E = ( Edg ` G )
3 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
4 2 3 eqtri 
 |-  E = ran ( iEdg ` G )
5 4 a1i 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> E = ran ( iEdg ` G ) )
6 5 fveq2d 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( # ` ran ( iEdg ` G ) ) )
7 1 opeq1i 
 |-  <. V , ( iEdg ` G ) >. = <. ( Vtx ` G ) , ( iEdg ` G ) >.
8 cusgrop 
 |-  ( G e. ComplUSGraph -> <. ( Vtx ` G ) , ( iEdg ` G ) >. e. ComplUSGraph )
9 7 8 eqeltrid 
 |-  ( G e. ComplUSGraph -> <. V , ( iEdg ` G ) >. e. ComplUSGraph )
10 fvex 
 |-  ( iEdg ` G ) e. _V
11 fvex 
 |-  ( Edg ` <. v , e >. ) e. _V
12 rabexg 
 |-  ( ( Edg ` <. v , e >. ) e. _V -> { c e. ( Edg ` <. v , e >. ) | n e/ c } e. _V )
13 12 resiexd 
 |-  ( ( Edg ` <. v , e >. ) e. _V -> ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) e. _V )
14 11 13 ax-mp 
 |-  ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) e. _V
15 rneq 
 |-  ( e = ( iEdg ` G ) -> ran e = ran ( iEdg ` G ) )
16 15 fveq2d 
 |-  ( e = ( iEdg ` G ) -> ( # ` ran e ) = ( # ` ran ( iEdg ` G ) ) )
17 fveq2 
 |-  ( v = V -> ( # ` v ) = ( # ` V ) )
18 17 oveq1d 
 |-  ( v = V -> ( ( # ` v ) _C 2 ) = ( ( # ` V ) _C 2 ) )
19 16 18 eqeqan12rd 
 |-  ( ( v = V /\ e = ( iEdg ` G ) ) -> ( ( # ` ran e ) = ( ( # ` v ) _C 2 ) <-> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) ) )
20 rneq 
 |-  ( e = f -> ran e = ran f )
21 20 fveq2d 
 |-  ( e = f -> ( # ` ran e ) = ( # ` ran f ) )
22 fveq2 
 |-  ( v = w -> ( # ` v ) = ( # ` w ) )
23 22 oveq1d 
 |-  ( v = w -> ( ( # ` v ) _C 2 ) = ( ( # ` w ) _C 2 ) )
24 21 23 eqeqan12rd 
 |-  ( ( v = w /\ e = f ) -> ( ( # ` ran e ) = ( ( # ` v ) _C 2 ) <-> ( # ` ran f ) = ( ( # ` w ) _C 2 ) ) )
25 vex 
 |-  v e. _V
26 vex 
 |-  e e. _V
27 25 26 opvtxfvi 
 |-  ( Vtx ` <. v , e >. ) = v
28 27 eqcomi 
 |-  v = ( Vtx ` <. v , e >. )
29 eqid 
 |-  ( Edg ` <. v , e >. ) = ( Edg ` <. v , e >. )
30 eqid 
 |-  { c e. ( Edg ` <. v , e >. ) | n e/ c } = { c e. ( Edg ` <. v , e >. ) | n e/ c }
31 eqid 
 |-  <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >. = <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >.
32 28 29 30 31 cusgrres 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ n e. v ) -> <. ( v \ { n } ) , ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) >. e. ComplUSGraph )
33 rneq 
 |-  ( f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) -> ran f = ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) )
34 33 fveq2d 
 |-  ( f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) -> ( # ` ran f ) = ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) )
35 34 adantl 
 |-  ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( # ` ran f ) = ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) )
36 fveq2 
 |-  ( w = ( v \ { n } ) -> ( # ` w ) = ( # ` ( v \ { n } ) ) )
37 36 adantr 
 |-  ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( # ` w ) = ( # ` ( v \ { n } ) ) )
38 37 oveq1d 
 |-  ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( ( # ` w ) _C 2 ) = ( ( # ` ( v \ { n } ) ) _C 2 ) )
39 35 38 eqeq12d 
 |-  ( ( w = ( v \ { n } ) /\ f = ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) -> ( ( # ` ran f ) = ( ( # ` w ) _C 2 ) <-> ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) )
40 edgopval 
 |-  ( ( v e. _V /\ e e. _V ) -> ( Edg ` <. v , e >. ) = ran e )
41 40 el2v 
 |-  ( Edg ` <. v , e >. ) = ran e
42 41 a1i 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( Edg ` <. v , e >. ) = ran e )
43 42 eqcomd 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ran e = ( Edg ` <. v , e >. ) )
44 43 fveq2d 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ran e ) = ( # ` ( Edg ` <. v , e >. ) ) )
45 cusgrusgr 
 |-  ( <. v , e >. e. ComplUSGraph -> <. v , e >. e. USGraph )
46 usgruhgr 
 |-  ( <. v , e >. e. USGraph -> <. v , e >. e. UHGraph )
47 45 46 syl 
 |-  ( <. v , e >. e. ComplUSGraph -> <. v , e >. e. UHGraph )
48 28 29 cusgrsizeindb0 
 |-  ( ( <. v , e >. e. UHGraph /\ ( # ` v ) = 0 ) -> ( # ` ( Edg ` <. v , e >. ) ) = ( ( # ` v ) _C 2 ) )
49 47 48 sylan 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ( Edg ` <. v , e >. ) ) = ( ( # ` v ) _C 2 ) )
50 44 49 eqtrd 
 |-  ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = 0 ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) )
51 rnresi 
 |-  ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) = { c e. ( Edg ` <. v , e >. ) | n e/ c }
52 51 fveq2i 
 |-  ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( # ` { c e. ( Edg ` <. v , e >. ) | n e/ c } )
53 41 a1i 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( Edg ` <. v , e >. ) = ran e )
54 53 rabeqdv 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> { c e. ( Edg ` <. v , e >. ) | n e/ c } = { c e. ran e | n e/ c } )
55 54 fveq2d 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( # ` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) = ( # ` { c e. ran e | n e/ c } ) )
56 52 55 eqtrid 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( # ` { c e. ran e | n e/ c } ) )
57 56 eqeq1d 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) <-> ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) )
58 57 biimpd 
 |-  ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) -> ( ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) -> ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) )
59 58 imdistani 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) )
60 41 eqcomi 
 |-  ran e = ( Edg ` <. v , e >. )
61 eqid 
 |-  { c e. ran e | n e/ c } = { c e. ran e | n e/ c }
62 28 60 61 cusgrsize2inds 
 |-  ( ( y + 1 ) e. NN0 -> ( ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) -> ( ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) ) ) )
63 62 imp31 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` { c e. ran e | n e/ c } ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) )
64 59 63 syl 
 |-  ( ( ( ( y + 1 ) e. NN0 /\ ( <. v , e >. e. ComplUSGraph /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ( # ` ran ( _I |` { c e. ( Edg ` <. v , e >. ) | n e/ c } ) ) = ( ( # ` ( v \ { n } ) ) _C 2 ) ) -> ( # ` ran e ) = ( ( # ` v ) _C 2 ) )
65 10 14 19 24 32 39 50 64 opfi1ind 
 |-  ( ( <. V , ( iEdg ` G ) >. e. ComplUSGraph /\ V e. Fin ) -> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) )
66 9 65 sylan 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` ran ( iEdg ` G ) ) = ( ( # ` V ) _C 2 ) )
67 6 66 eqtrd 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( # ` E ) = ( ( # ` V ) _C 2 ) )