Metamath Proof Explorer

Theorem cusgrsizeinds

Description: Part 1 of induction step in cusgrsize . The size of a complete simple graph with n vertices is ( n - 1 ) plus the size of the complete graph reduced by one vertex. (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
cusgrsizeinds.f ⊢ F = e ∈ E | N ∉ e
Assertion cusgrsizeinds ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → E = V - 1 + F

Proof

Step Hyp Ref Expression
1 cusgrsizeindb0.v ⊢ V = Vtx ⁡ G
2 cusgrsizeindb0.e ⊢ E = Edg ⁡ G
3 cusgrsizeinds.f ⊢ F = e ∈ E | N ∉ e
4 cusgrusgr ⊢ G ∈ ComplUSGraph → G ∈ USGraph
5 1 isfusgr ⊢ G ∈ FinUSGraph ↔ G ∈ USGraph ∧ V ∈ Fin
6 fusgrfis ⊢ G ∈ FinUSGraph → Edg ⁡ G ∈ Fin
7 5 6 sylbir ⊢ G ∈ USGraph ∧ V ∈ Fin → Edg ⁡ G ∈ Fin
8 7 a1d ⊢ G ∈ USGraph ∧ V ∈ Fin → N ∈ V → Edg ⁡ G ∈ Fin
9 8 ex ⊢ G ∈ USGraph → V ∈ Fin → N ∈ V → Edg ⁡ G ∈ Fin
10 4 9 syl ⊢ G ∈ ComplUSGraph → V ∈ Fin → N ∈ V → Edg ⁡ G ∈ Fin
11 10 3imp ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → Edg ⁡ G ∈ Fin
12 eqid ⊢ e ∈ E | N ∈ e = e ∈ E | N ∈ e
13 12 3 elnelun ⊢ e ∈ E | N ∈ e ∪ F = E
14 13 eqcomi ⊢ E = e ∈ E | N ∈ e ∪ F
15 14 fveq2i ⊢ E = e ∈ E | N ∈ e ∪ F
16 15 a1i ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → E = e ∈ E | N ∈ e ∪ F
17 2 eqcomi ⊢ Edg ⁡ G = E
18 17 eleq1i ⊢ Edg ⁡ G ∈ Fin ↔ E ∈ Fin
19 rabfi ⊢ E ∈ Fin → e ∈ E | N ∈ e ∈ Fin
20 18 19 sylbi ⊢ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e ∈ Fin
21 20 adantl ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e ∈ Fin
22 4 anim1i ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin → G ∈ USGraph ∧ V ∈ Fin
23 22 5 sylibr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin → G ∈ FinUSGraph
24 1 2 3 usgrfilem ⊢ G ∈ FinUSGraph ∧ N ∈ V → E ∈ Fin ↔ F ∈ Fin
25 23 24 stoic3 ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → E ∈ Fin ↔ F ∈ Fin
26 18 25 bitrid ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → Edg ⁡ G ∈ Fin ↔ F ∈ Fin
27 26 biimpa ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → F ∈ Fin
28 12 3 elneldisj ⊢ e ∈ E | N ∈ e ∩ F = ∅
29 28 a1i ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e ∩ F = ∅
30 hashun ⊢ e ∈ E | N ∈ e ∈ Fin ∧ F ∈ Fin ∧ e ∈ E | N ∈ e ∩ F = ∅ → e ∈ E | N ∈ e ∪ F = e ∈ E | N ∈ e + F
31 21 27 29 30 syl3anc ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e ∪ F = e ∈ E | N ∈ e + F
32 1 2 cusgrsizeindslem ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → e ∈ E | N ∈ e = V − 1
33 32 adantr ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e = V − 1
34 33 oveq1d ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → e ∈ E | N ∈ e + F = V - 1 + F
35 16 31 34 3eqtrd ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V ∧ Edg ⁡ G ∈ Fin → E = V - 1 + F
36 11 35 mpdan ⊢ G ∈ ComplUSGraph ∧ V ∈ Fin ∧ N ∈ V → E = V - 1 + F