Theorem usgrfilem

Description: In a finite simple graph, the number of edges is finite iff the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 9-Nov-2020)

	Ref	Expression
Hypotheses	fusgredgfi.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	usgrfilem.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
Assertion	usgrfilem	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ∈ Fin ↔ 𝐹 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		fusgredgfi.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		fusgredgfi.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		usgrfilem.f	⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4		rabfi	⊢ ( 𝐸 ∈ Fin → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 } ∈ Fin )
5	3 4	eqeltrid	⊢ ( 𝐸 ∈ Fin → 𝐹 ∈ Fin )
6		uncom	⊢ ( 𝐹 ∪ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) = ( { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∪ 𝐹 )
7		eqid	⊢ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
8	7 3	elnelun	⊢ ( { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∪ 𝐹 ) = 𝐸
9	6 8	eqtr2i	⊢ 𝐸 = ( 𝐹 ∪ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } )
10	1 2	fusgredgfi	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin )
11	10	anim1ci	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐹 ∈ Fin ) → ( 𝐹 ∈ Fin ∧ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin ) )
12		unfi	⊢ ( ( 𝐹 ∈ Fin ∧ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ∈ Fin ) → ( 𝐹 ∪ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ∈ Fin )
13	11 12	syl	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐹 ∈ Fin ) → ( 𝐹 ∪ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ∈ Fin )
14	9 13	eqeltrid	⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐹 ∈ Fin ) → 𝐸 ∈ Fin )
15	14	ex	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐹 ∈ Fin → 𝐸 ∈ Fin ) )
16	5 15	impbid2	⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ∈ Fin ↔ 𝐹 ∈ Fin ) )