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	syl5bi	⊢ ( ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) ∧ ⟨ 𝑉 , 𝐸 ⟩ ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∣ 𝑁 ∉ 𝑝 } ) ∈ Fin → 𝐸 ∈ Fin ) )