nbupgrres

Description: The neighborhood of a vertex in a restricted pseudograph (not necessarily valid for a hypergraph, because N , K and M could be connected by one edge, so M is a neighbor of K in the original graph, but not in the restricted graph, because the edge between M and K , also incident with N , was removed). (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		nbupgrres.v	$⊢ V = Vtx (G)$
2		nbupgrres.e	$⊢ E = Edg (G)$
3		nbupgrres.f	$⊢ F = \{e \in E \| N \notin e\}$
4		nbupgrres.s	$⊢ S = ⟨V ∖ \{N\}, {I ↾}_{F}⟩$
5		simp1l	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to G \in UPGraph$
6		eldifi	$⊢ K \in (V ∖ \{N\}) \to K \in V$
7	6	3ad2ant2	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to K \in V$
8		eldifsn	$⊢ M \in ((V ∖ \{N\}) ∖ \{K\}) \leftrightarrow (M \in (V ∖ \{N\}) \land M \neq K)$
9		eldifi	$⊢ M \in (V ∖ \{N\}) \to M \in V$
10	9	anim1i	$⊢ (M \in (V ∖ \{N\}) \land M \neq K) \to (M \in V \land M \neq K)$
11	8 10	sylbi	$⊢ M \in ((V ∖ \{N\}) ∖ \{K\}) \to (M \in V \land M \neq K)$
12		difpr	$⊢ V ∖ \{N, K\} = (V ∖ \{N\}) ∖ \{K\}$
13	11 12	eleq2s	$⊢ M \in (V ∖ \{N, K\}) \to (M \in V \land M \neq K)$
14	13	3ad2ant3	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to (M \in V \land M \neq K)$
15	1 2	nbupgrel	$⊢ ((G \in UPGraph \land K \in V) \land (M \in V \land M \neq K)) \to (M \in (G NeighbVtx K) \leftrightarrow \{M, K\} \in E)$
16	5 7 14 15	syl21anc	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to (M \in (G NeighbVtx K) \leftrightarrow \{M, K\} \in E)$
17	16	biimpa	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to \{M, K\} \in E$
18	12	eleq2i	$⊢ M \in (V ∖ \{N, K\}) \leftrightarrow M \in ((V ∖ \{N\}) ∖ \{K\})$
19		eldifsn	$⊢ M \in (V ∖ \{N\}) \leftrightarrow (M \in V \land M \neq N)$
20	19	anbi1i	$⊢ (M \in (V ∖ \{N\}) \land M \neq K) \leftrightarrow ((M \in V \land M \neq N) \land M \neq K)$
21	18 8 20	3bitri	$⊢ M \in (V ∖ \{N, K\}) \leftrightarrow ((M \in V \land M \neq N) \land M \neq K)$
22		simpr	$⊢ (M \in V \land M \neq N) \to M \neq N$
23	22	necomd	$⊢ (M \in V \land M \neq N) \to N \neq M$
24	23	adantr	$⊢ ((M \in V \land M \neq N) \land M \neq K) \to N \neq M$
25	21 24	sylbi	$⊢ M \in (V ∖ \{N, K\}) \to N \neq M$
26	25	3ad2ant3	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to N \neq M$
27		eldifsn	$⊢ K \in (V ∖ \{N\}) \leftrightarrow (K \in V \land K \neq N)$
28		simpr	$⊢ (K \in V \land K \neq N) \to K \neq N$
29	28	necomd	$⊢ (K \in V \land K \neq N) \to N \neq K$
30	27 29	sylbi	$⊢ K \in (V ∖ \{N\}) \to N \neq K$
31	30	3ad2ant2	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to N \neq K$
32	26 31	nelprd	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to \neg N \in \{M, K\}$
33		df-nel	$⊢ N \notin \{M, K\} \leftrightarrow \neg N \in \{M, K\}$
34	32 33	sylibr	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to N \notin \{M, K\}$
35	34	adantr	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to N \notin \{M, K\}$
36		neleq2	$⊢ e = \{M, K\} \to (N \notin e \leftrightarrow N \notin \{M, K\})$
37	36 3	elrab2	$⊢ \{M, K\} \in F \leftrightarrow (\{M, K\} \in E \land N \notin \{M, K\})$
38	17 35 37	sylanbrc	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to \{M, K\} \in F$
39	1 2 3 4	upgrres1	$⊢ (G \in UPGraph \land N \in V) \to S \in UPGraph$
40	39	3ad2ant1	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to S \in UPGraph$
41		simp2	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to K \in (V ∖ \{N\})$
42	18 8	sylbb	$⊢ M \in (V ∖ \{N, K\}) \to (M \in (V ∖ \{N\}) \land M \neq K)$
43	42	3ad2ant3	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to (M \in (V ∖ \{N\}) \land M \neq K)$
44	40 41 43	jca31	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to ((S \in UPGraph \land K \in (V ∖ \{N\})) \land (M \in (V ∖ \{N\}) \land M \neq K))$
45	44	adantr	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to ((S \in UPGraph \land K \in (V ∖ \{N\})) \land (M \in (V ∖ \{N\}) \land M \neq K))$
46	1 2 3 4	upgrres1lem2	$⊢ Vtx (S) = V ∖ \{N\}$
47	46	eqcomi	$⊢ V ∖ \{N\} = Vtx (S)$
48		edgval	$⊢ Edg (S) = ran iEdg (S)$
49	1 2 3 4	upgrres1lem3	$⊢ iEdg (S) = {I ↾}_{F}$
50	49	rneqi	$⊢ ran iEdg (S) = ran ({I ↾}_{F})$
51		rnresi	$⊢ ran ({I ↾}_{F}) = F$
52	48 50 51	3eqtrri	$⊢ F = Edg (S)$
53	47 52	nbupgrel	$⊢ ((S \in UPGraph \land K \in (V ∖ \{N\})) \land (M \in (V ∖ \{N\}) \land M \neq K)) \to (M \in (S NeighbVtx K) \leftrightarrow \{M, K\} \in F)$
54	45 53	syl	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to (M \in (S NeighbVtx K) \leftrightarrow \{M, K\} \in F)$
55	38 54	mpbird	$⊢ (((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \land M \in (G NeighbVtx K)) \to M \in (S NeighbVtx K)$
56	55	ex	$⊢ ((G \in UPGraph \land N \in V) \land K \in (V ∖ \{N\}) \land M \in (V ∖ \{N, K\})) \to (M \in (G NeighbVtx K) \to M \in (S NeighbVtx K))$

Metamath Proof Explorer

Theorem nbupgrres

Proof