This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )