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 ) )