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