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→GNeighbVtxN=V∖N
5 3 4 sylan ⊢G∈ComplUSGraph∧N∈V→GNeighbVtxN=V∖N
6 5 3adant2 ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→GNeighbVtxN=V∖N
7 6 fveq2d ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→GNeighbVtxN=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→∃ff:GNeighbVtxN⟶1-1 ontoe∈E|N∈e
12 10 11 syl ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→∃ff:GNeighbVtxN⟶1-1 ontoe∈E|N∈e
13 1 2 nbusgr ⊢G∈USGraph→GNeighbVtxN=n∈V|Nn∈E
14 8 13 syl ⊢G∈ComplUSGraph→GNeighbVtxN=n∈V|Nn∈E
15 14 adantr ⊢G∈ComplUSGraph∧V∈Fin→GNeighbVtxN=n∈V|Nn∈E
16 rabfi ⊢V∈Fin→n∈V|Nn∈E∈Fin
17 16 adantl ⊢G∈ComplUSGraph∧V∈Fin→n∈V|Nn∈E∈Fin
18 15 17 eqeltrd ⊢G∈ComplUSGraph∧V∈Fin→GNeighbVtxN∈Fin
19 18 3adant3 ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→GNeighbVtxN∈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 ⊢GNeighbVtxN∈Fin∧e∈E|N∈e∈Fin→GNeighbVtxN=e∈E|N∈e↔∃ff:GNeighbVtxN⟶1-1 ontoe∈E|N∈e
30 19 28 29 syl2anc ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→GNeighbVtxN=e∈E|N∈e↔∃ff:GNeighbVtxN⟶1-1 ontoe∈E|N∈e
31 12 30 mpbird ⊢G∈ComplUSGraph∧V∈Fin∧N∈V→GNeighbVtxN=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