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 ComplUSGraph V Fin N V e E | N e = V 1

Proof

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