nbupgruvtxres

Description: The neighborhood of a universal vertex in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		nbupgruvtxres.v	$⊢ V = Vtx (G)$
2		nbupgruvtxres.e	$⊢ E = Edg (G)$
3		nbupgruvtxres.f	$⊢ F = \{e \in E \| N \notin e\}$
4		nbupgruvtxres.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
5		eqid	$⊢ Vtx (S) = Vtx (S)$
6	5	nbgrssovtx	$⊢ S NeighbVtx K \subseteq Vtx (S) ∖ \{K\}$
7		difpr	$⊢ V ∖ \{N, K\} = (V ∖ \{N\}) ∖ \{K\}$
8	1 2 3 4	upgrres1lem2	$⊢ Vtx (S) = V ∖ \{N\}$
9	8	eqcomi	$⊢ V ∖ \{N\} = Vtx (S)$
10	9	a1i	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \to V ∖ \{N\} = Vtx (S)$
11	10	difeq1d	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \to (V ∖ \{N\}) ∖ \{K\} = Vtx (S) ∖ \{K\}$
12	7 11	syl5eq	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \to V ∖ \{N, K\} = Vtx (S) ∖ \{K\}$
13	6 12	sseqtrrid	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \to S NeighbVtx K \subseteq V ∖ \{N, K\}$
14	13	adantr	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \to S NeighbVtx K \subseteq V ∖ \{N, K\}$
15		simpl	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \to ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}))$
16	15	anim1i	$⊢ ((((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \land n \in (V ∖ \{N, K\})) \to (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land n \in (V ∖ \{N, K\}))$
17		df-3an	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land n \in (V ∖ \{N, K\})) \leftrightarrow (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land n \in (V ∖ \{N, K\}))$
18	16 17	sylibr	$⊢ ((((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \land n \in (V ∖ \{N, K\})) \to ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land n \in (V ∖ \{N, K\}))$
19		dif32	$⊢ (V ∖ \{N\}) ∖ \{K\} = (V ∖ \{K\}) ∖ \{N\}$
20	7 19	eqtri	$⊢ V ∖ \{N, K\} = (V ∖ \{K\}) ∖ \{N\}$
21	20	eleq2i	$⊢ n \in (V ∖ \{N, K\}) \leftrightarrow n \in ((V ∖ \{K\}) ∖ \{N\})$
22		eldifsn	$⊢ n \in ((V ∖ \{K\}) ∖ \{N\}) \leftrightarrow (n \in (V ∖ \{K\}) \land n \neq N)$
23	21 22	bitri	$⊢ n \in (V ∖ \{N, K\}) \leftrightarrow (n \in (V ∖ \{K\}) \land n \neq N)$
24	23	simplbi	$⊢ n \in (V ∖ \{N, K\}) \to n \in (V ∖ \{K\})$
25		eleq2	$⊢ G NeighbVtx K = V ∖ \{K\} \to (n \in (G NeighbVtx K) \leftrightarrow n \in (V ∖ \{K\}))$
26	24 25	syl5ibr	$⊢ G NeighbVtx K = V ∖ \{K\} \to (n \in (V ∖ \{N, K\}) \to n \in (G NeighbVtx K))$
27	26	adantl	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \to (n \in (V ∖ \{N, K\}) \to n \in (G NeighbVtx K))$
28	27	imp	$⊢ ((((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \land n \in (V ∖ \{N, K\})) \to n \in (G NeighbVtx K)$
29	1 2 3 4	nbupgrres	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land n \in (V ∖ \{N, K\})) \to (n \in (G NeighbVtx K) \to n \in (S NeighbVtx K))$
30	18 28 29	sylc	$⊢ ((((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \land n \in (V ∖ \{N, K\})) \to n \in (S NeighbVtx K)$
31	14 30	eqelssd	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \land G NeighbVtx K = V ∖ \{K\}) \to S NeighbVtx K = V ∖ \{N, K\}$
32	31	ex	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\})) \to (G NeighbVtx K = V ∖ \{K\} \to S NeighbVtx K = V ∖ \{N, K\})$

Metamath Proof Explorer

Theorem nbupgruvtxres

Proof