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	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to ({I ↾}_{\{p \in Edg (⟨V, E⟩) \| N \notin p\}} \in Fin \to E \in Fin)$

Proof

Step	Hyp	Ref	Expression
1		residfi	$⊢ {I ↾}_{\{p \in Edg (⟨V, E⟩) \| N \notin p\}} \in Fin \leftrightarrow \{p \in Edg (⟨V, E⟩) \| N \notin p\} \in Fin$
2		fusgrusgr	$⊢ ⟨V, E⟩ \in FinUSGraph \to ⟨V, E⟩ \in USGraph$
3		eqid	$⊢ iEdg (⟨V, E⟩) = iEdg (⟨V, E⟩)$
4		eqid	$⊢ Edg (⟨V, E⟩) = Edg (⟨V, E⟩)$
5	3 4	usgredgffibi	$⊢ ⟨V, E⟩ \in USGraph \to (Edg (⟨V, E⟩) \in Fin \leftrightarrow iEdg (⟨V, E⟩) \in Fin)$
6	2 5	syl	$⊢ ⟨V, E⟩ \in FinUSGraph \to (Edg (⟨V, E⟩) \in Fin \leftrightarrow iEdg (⟨V, E⟩) \in Fin)$
7	6	3ad2ant2	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to (Edg (⟨V, E⟩) \in Fin \leftrightarrow iEdg (⟨V, E⟩) \in Fin)$
8		simp2	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to ⟨V, E⟩ \in FinUSGraph$
9		opvtxfv	$⊢ (V \in X \land E \in Y) \to Vtx (⟨V, E⟩) = V$
10	9	eqcomd	$⊢ (V \in X \land E \in Y) \to V = Vtx (⟨V, E⟩)$
11	10	eleq2d	$⊢ (V \in X \land E \in Y) \to (N \in V \leftrightarrow N \in Vtx (⟨V, E⟩))$
12	11	biimpa	$⊢ ((V \in X \land E \in Y) \land N \in V) \to N \in Vtx (⟨V, E⟩)$
13		eqid	$⊢ Vtx (⟨V, E⟩) = Vtx (⟨V, E⟩)$
14		eqid	$⊢ \{p \in Edg (⟨V, E⟩) \| N \notin p\} = \{p \in Edg (⟨V, E⟩) \| N \notin p\}$
15	13 4 14	usgrfilem	$⊢ (⟨V, E⟩ \in FinUSGraph \land N \in Vtx (⟨V, E⟩)) \to (Edg (⟨V, E⟩) \in Fin \leftrightarrow \{p \in Edg (⟨V, E⟩) \| N \notin p\} \in Fin)$
16	8 12 15	3imp3i2an	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to (Edg (⟨V, E⟩) \in Fin \leftrightarrow \{p \in Edg (⟨V, E⟩) \| N \notin p\} \in Fin)$
17		opiedgfv	$⊢ (V \in X \land E \in Y) \to iEdg (⟨V, E⟩) = E$
18	17	eleq1d	$⊢ (V \in X \land E \in Y) \to (iEdg (⟨V, E⟩) \in Fin \leftrightarrow E \in Fin)$
19	18	3ad2ant1	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to (iEdg (⟨V, E⟩) \in Fin \leftrightarrow E \in Fin)$
20	7 16 19	3bitr3rd	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to (E \in Fin \leftrightarrow \{p \in Edg (⟨V, E⟩) \| N \notin p\} \in Fin)$
21	20	biimprd	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to (\{p \in Edg (⟨V, E⟩) \| N \notin p\} \in Fin \to E \in Fin)$
22	1 21	syl5bi	$⊢ ((V \in X \land E \in Y) \land ⟨V, E⟩ \in FinUSGraph \land N \in V) \to ({I ↾}_{\{p \in Edg (⟨V, E⟩) \| N \notin p\}} \in Fin \to E \in Fin)$

Metamath Proof Explorer

Theorem fusgrfisstep

Proof