Metamath Proof Explorer

Theorem cusgrsizeindslem

Description: Lemma for cusgrsizeinds . (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 )
Assertion cusgrsizeindslem 
|- ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` { e e. E | N e. e } ) = ( ( # ` V ) - 1 ) )

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v 
 |-  V = ( Vtx ` G )
2 cusgrsizeindb0.e 
 |-  E = ( Edg ` G )
3 cusgrcplgr 
 |-  ( G e. ComplUSGraph -> G e. ComplGraph )
4 1 nbcplgr 
 |-  ( ( G e. ComplGraph /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
5 3 4 sylan 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
6 5 3adant2 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
7 6 fveq2d 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` ( G NeighbVtx N ) ) = ( # ` ( V \ { N } ) ) )
8 cusgrusgr 
 |-  ( G e. ComplUSGraph -> G e. USGraph )
9 8 anim1i 
 |-  ( ( G e. ComplUSGraph /\ N e. V ) -> ( G e. USGraph /\ N e. V ) )
10 9 3adant2 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( G e. USGraph /\ N e. V ) )
11 1 2 nbusgrf1o 
 |-  ( ( G e. USGraph /\ N e. V ) -> E. f f : ( G NeighbVtx N ) -1-1-onto-> { e e. E | N e. e } )
12 10 11 syl 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> E. f f : ( G NeighbVtx N ) -1-1-onto-> { e e. E | N e. e } )
13 1 2 nbusgr 
 |-  ( G e. USGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
14 8 13 syl 
 |-  ( G e. ComplUSGraph -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
15 14 adantr 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( G NeighbVtx N ) = { n e. V | { N , n } e. E } )
16 rabfi 
 |-  ( V e. Fin -> { n e. V | { N , n } e. E } e. Fin )
17 16 adantl 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> { n e. V | { N , n } e. E } e. Fin )
18 15 17 eqeltrd 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( G NeighbVtx N ) e. Fin )
19 18 3adant3 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( G NeighbVtx N ) e. Fin )
20 8 anim1i 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> ( G e. USGraph /\ V e. Fin ) )
21 1 isfusgr 
 |-  ( G e. FinUSGraph <-> ( G e. USGraph /\ V e. Fin ) )
22 20 21 sylibr 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> G e. FinUSGraph )
23 fusgrfis 
 |-  ( G e. FinUSGraph -> ( Edg ` G ) e. Fin )
24 2 23 eqeltrid 
 |-  ( G e. FinUSGraph -> E e. Fin )
25 rabfi 
 |-  ( E e. Fin -> { e e. E | N e. e } e. Fin )
26 24 25 syl 
 |-  ( G e. FinUSGraph -> { e e. E | N e. e } e. Fin )
27 22 26 syl 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin ) -> { e e. E | N e. e } e. Fin )
28 27 3adant3 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> { e e. E | N e. e } e. Fin )
29 hasheqf1o 
 |-  ( ( ( G NeighbVtx N ) e. Fin /\ { e e. E | N e. e } e. Fin ) -> ( ( # ` ( G NeighbVtx N ) ) = ( # ` { e e. E | N e. e } ) <-> E. f f : ( G NeighbVtx N ) -1-1-onto-> { e e. E | N e. e } ) )
30 19 28 29 syl2anc 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( ( # ` ( G NeighbVtx N ) ) = ( # ` { e e. E | N e. e } ) <-> E. f f : ( G NeighbVtx N ) -1-1-onto-> { e e. E | N e. e } ) )
31 12 30 mpbird 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` ( G NeighbVtx N ) ) = ( # ` { e e. E | N e. e } ) )
32 hashdifsn 
 |-  ( ( V e. Fin /\ N e. V ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - 1 ) )
33 32 3adant1 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` ( V \ { N } ) ) = ( ( # ` V ) - 1 ) )
34 7 31 33 3eqtr3d 
 |-  ( ( G e. ComplUSGraph /\ V e. Fin /\ N e. V ) -> ( # ` { e e. E | N e. e } ) = ( ( # ` V ) - 1 ) )