Metamath Proof Explorer

Theorem cusgrsizeinds

Description: Part 1 of induction step in cusgrsize . The size of a complete simple graph with n vertices is ( n - 1 ) plus the size of the complete graph reduced by one vertex. (Contributed by Alexander van der Vekens, 11-Jan-2018) (Revised by AV, 9-Nov-2020)

Ref Expression
Hypotheses cusgrsizeindb0.v 
|- V = ( Vtx ` G )
cusgrsizeindb0.e 
|- E = ( Edg ` G )
cusgrsizeinds.f 
|- F = { e e. E | N e/ e }
Assertion cusgrsizeinds 
|- ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` E ) = ( ( ( # ` V ) - 1 ) + ( # ` F ) ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v 
 |-  V = ( Vtx ` G )
2 cusgrsizeindb0.e 
 |-  E = ( Edg ` G )
3 cusgrsizeinds.f 
 |-  F = { e e. E | N e/ e }
4 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
5 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
6 fusgrfis 
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
7 5 6 sylbir 
 |-  ( ( G e. USGraph /\ V e. Fin ) -> ( Edg ` G ) e. Fin )
8 7 a1d 
 |-  ( ( G e. USGraph /\ V e. Fin ) -> ( N e. V -> ( Edg ` G ) e. Fin ) )
9 8 ex 
 |-  ( G e. USGraph -> ( V e. Fin -> ( N e. V -> ( Edg ` G ) e. Fin ) ) )
10 4 9 syl 
 |-  ( G e. ComplUSGraph -> ( V e. Fin -> ( N e. V -> ( Edg ` G ) e. Fin ) ) )
11 10 3imp 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( Edg ` G ) e. Fin )
12 eqid 
 |-  { e e. E | N e. e } = { e e. E | N e. e }
13 12 3 elnelun 
 |-  ( { e e. E | N e. e } u. F ) = E
14 13 eqcomi 
 |-  E = ( { e e. E | N e. e } u. F )
15 14 fveq2i 
 |-  ( # ` E ) = ( # ` ( { e e. E | N e. e } u. F ) )
16 15 a1i 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( # ` E ) = ( # ` ( { e e. E | N e. e } u. F ) ) )
17 2 eqcomi 
 |-  ( Edg ` G ) = E
18 17 eleq1i 
 |-  ( ( Edg ` G ) e. Fin <-> E e. Fin )
19 rabfi 
 |-  ( E e. Fin -> { e e. E | N e. e } e. Fin )
20 18 19 sylbi 
 |-  ( ( Edg ` G ) e. Fin -> { e e. E | N e. e } e. Fin )
21 20 adantl 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> { e e. E | N e. e } e. Fin )
22 4 anim1i 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( G e. USGraph /\ V e. Fin ) )
23 22 5 sylibr 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> G e. FinUSGraph )
24 1 2 3 usgrfilem 
 |-  ( ( G e. FinUSGraph /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
25 23 24 stoic3 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( E e. Fin <-> F e. Fin ) )
26 18 25 syl5bb 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( ( Edg ` G ) e. Fin <-> F e. Fin ) )
27 26 biimpa 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> F e. Fin )
28 12 3 elneldisj 
 |-  ( { e e. E | N e. e } i^i F ) = (/)
29 28 a1i 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( { e e. E | N e. e } i^i F ) = (/) )
30 hashun 
 |-  ( ( { e e. E | N e. e } e. Fin /\ F e. Fin /\ ( { e e. E | N e. e } i^i F ) = (/) ) -> ( # ` ( { e e. E | N e. e } u. F ) ) = ( ( # ` { e e. E | N e. e } ) + ( # ` F ) ) )
31 21 27 29 30 syl3anc 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( # ` ( { e e. E | N e. e } u. F ) ) = ( ( # ` { e e. E | N e. e } ) + ( # ` F ) ) )
32 1 2 cusgrsizeindslem 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` { e e. E | N e. e } ) = ( ( # ` V ) - 1 ) )
33 32 adantr 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( # ` { e e. E | N e. e } ) = ( ( # ` V ) - 1 ) )
34 33 oveq1d 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( ( # ` { e e. E | N e. e } ) + ( # ` F ) ) = ( ( ( # ` V ) - 1 ) + ( # ` F ) ) )
35 16 31 34 3eqtrd 
 |-  ( ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) /\ ( Edg ` G ) e. Fin ) -> ( # ` E ) = ( ( ( # ` V ) - 1 ) + ( # ` F ) ) )
36 11 35 mpdan 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` E ) = ( ( ( # ` V ) - 1 ) + ( # ` F ) ) )