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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	cusgrsizeindb0.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	cusgrsizeinds.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
Assertion	cusgrsizeinds	⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ 𝐸 ) = ( ( ( ♯ ‘ 𝑉 ) − 1 ) + ( ♯ ‘ 𝐹 ) ) )

Proof

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

Metamath Proof Explorer

Theorem cusgrsizeinds

Proof