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

Metamath Proof Explorer

Theorem fusgrfisstep

Description: Induction step in fusgrfis : In a finite simple graph, the number of edges is finite if the number of edges not containing one of the vertices is finite. (Contributed by Alexander van der Vekens, 5-Jan-2018) (Revised by AV, 23-Oct-2020)

Ref Expression
Assertion fusgrfisstep ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ) ∈ Fin → 𝐸 ∈ Fin ) )

Proof

Step Hyp Ref Expression
1 residfi ⊢ ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ) ∈ Fin ↔ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ∈ Fin )
2 fusgrusgr ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph → ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph )
3 eqid ⊢ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
4 eqid ⊢ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
5 3 4 usgredgffibi ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
6 2 5 syl ⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
7 6 3ad2ant2 ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ) )
8 simp2 ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph )
9 opvtxfv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
10 9 eqcomd ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝑉 = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
11 10 eleq2d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ) )
12 11 biimpa ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) )
13 eqid ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
14 eqid ⊢ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } = { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 }
15 13 4 14 usgrfilem ⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ) → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ∈ Fin ) )
16 8 12 15 3imp3i2an ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ∈ Fin ) )
17 opiedgfv ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
18 17 eleq1d ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ 𝐸 ∈ Fin ) )
19 18 3ad2ant1 ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∈ Fin ↔ 𝐸 ∈ Fin ) )
20 7 16 19 3bitr3rd ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐸 ∈ Fin ↔ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ∈ Fin ) )
21 20 biimprd ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ∈ Fin → 𝐸 ∈ Fin ) )
22 1 21 biimtrid ⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ) ∈ Fin → 𝐸 ∈ Fin ) )