usgrres1

Description: Restricting a simple graph by removing one vertex results in a simple graph. Remark: This restricted 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 Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 10-Jan-2020) (Revised by AV, 23-Oct-2020) (Proof shortened 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	usgrres1	$⊢ (G \in USGraph \land N \in V) \to S \in USGraph$

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		f1of1	$⊢ ({I ↾}_{F}) : F \underset{1-1 onto}{⟶} F \to ({I ↾}_{F}) : F \underset{1-1}{⟶} F$
7	5 6	mp1i	$⊢ (G \in USGraph \land N \in V) \to ({I ↾}_{F}) : F \underset{1-1}{⟶} F$
8		eqidd	$⊢ (G \in USGraph \land N \in V) \to {I ↾}_{F} = {I ↾}_{F}$
9		dmresi	$⊢ dom ({I ↾}_{F}) = F$
10	9	a1i	$⊢ (G \in USGraph \land N \in V) \to dom ({I ↾}_{F}) = F$
11		eqidd	$⊢ (G \in USGraph \land N \in V) \to F = F$
12	8 10 11	f1eq123d	$⊢ (G \in USGraph \land N \in V) \to (({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} F \leftrightarrow ({I ↾}_{F}) : F \underset{1-1}{⟶} F)$
13	7 12	mpbird	$⊢ (G \in USGraph \land N \in V) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} F$
14		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
15	1 2 3	umgrres1lem	$⊢ (G \in UMGraph \land N \in V) \to ran ({I ↾}_{F}) \subseteq \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
16	14 15	sylan	$⊢ (G \in USGraph \land N \in V) \to ran ({I ↾}_{F}) \subseteq \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
17		f1ssr	$⊢ (({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} F \land ran ({I ↾}_{F}) \subseteq \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
18	13 16 17	syl2anc	$⊢ (G \in USGraph \land N \in V) \to ({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\}$
19		opex	$⊢ ⟨V ∖ \{N\}, {I ↾}_{F}⟩ \in V$
20	4 19	eqeltri	$⊢ S \in V$
21	1 2 3 4	upgrres1lem2	$⊢ Vtx (S) = V ∖ \{N\}$
22	21	eqcomi	$⊢ V ∖ \{N\} = Vtx (S)$
23	1 2 3 4	upgrres1lem3	$⊢ iEdg (S) = {I ↾}_{F}$
24	23	eqcomi	$⊢ {I ↾}_{F} = iEdg (S)$
25	22 24	isusgrs	$⊢ S \in V \to (S \in USGraph \leftrightarrow ({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\})$
26	20 25	mp1i	$⊢ (G \in USGraph \land N \in V) \to (S \in USGraph \leftrightarrow ({I ↾}_{F}) : dom ({I ↾}_{F}) \underset{1-1}{⟶} \{p \in 𝒫 (V ∖ \{N\}) \| \|p\| = 2\})$
27	18 26	mpbird	$⊢ (G \in USGraph \land N \in V) \to S \in USGraph$

Metamath Proof Explorer

Theorem usgrres1

Proof