umgrres1

Description: A multigraph obtained by removing one vertex and all edges incident with this vertex is a multigraph. Remark: This graph is not a subgraph of the original graph in the sense of df-subgr since the domains of the edge functions may not be compatible. (Contributed by AV, 27-Nov-2020)

	Ref	Expression
Hypotheses	upgrres1.v	$⊢ V = Vtx (G)$
	upgrres1.e	$⊢ E = Edg (G)$
	upgrres1.f	$⊢ F = \{e \in E \| N \notin e\}$
	upgrres1.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
Assertion	umgrres1	$⊢ (G \in UMGraph \land N \in V) \to S \in UMGraph$

Proof

Step	Hyp	Ref	Expression
1		upgrres1.v	$⊢ V = Vtx (G)$
2		upgrres1.e	$⊢ E = Edg (G)$
3		upgrres1.f	$⊢ F = \{e \in E \| N \notin e\}$
4		upgrres1.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
5		f1oi	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F$
6		f1of	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F \to ({I ↾}_{F}) : F ⟶ F$
7	5 6	mp1i	$⊢ (G \in UMGraph \land N \in V) \to ({I ↾}_{F}) : F ⟶ F$
8	7	ffdmd	$⊢ (G \in UMGraph \land N \in V) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ F$
9		rnresi	$⊢ ran ({I ↾}_{F}) = F$
10	1 2 3	umgrres1lem	$⊢ (G \in UMGraph \land N \in V) \to ran ({I ↾}_{F}) \subseteq \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
11	9 10	eqsstrrid	$⊢ (G \in UMGraph \land N \in V) \to F \subseteq \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
12	8 11	fssd	$⊢ (G \in UMGraph \land N \in V) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
13		opex	$⊢ ⟨V ∖ \{N\}, {I ↾}_{F}⟩ \in V$
14	4 13	eqeltri	$⊢ S \in V$
15	1 2 3 4	upgrres1lem2	$⊢ Vtx (S) = V ∖ \{N\}$
16	15	eqcomi	$⊢ V ∖ \{N\} = Vtx (S)$
17	1 2 3 4	upgrres1lem3	$⊢ iEdg (S) = {I ↾}_{F}$
18	17	eqcomi	$⊢ {I ↾}_{F} = iEdg (S)$
19	16 18	isumgrs	$⊢ S \in V \to (S \in UMGraph \leftrightarrow ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\})$
20	14 19	mp1i	$⊢ (G \in UMGraph \land N \in V) \to (S \in UMGraph \leftrightarrow ({I ↾}_{F}) : dom ({I ↾}_{F}) ⟶ \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\})$
21	12 20	mpbird	$⊢ (G \in UMGraph \land N \in V) \to S \in UMGraph$

Metamath Proof Explorer

Theorem umgrres1

Proof