fusgr2wsp2nb

Description: The set of paths of length 2 with a given vertex in the middle for a finite simple graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018) (Revised by AV, 17-May-2021) (Proof shortened by AV, 16-Mar-2022)

	Ref	Expression
Hypotheses	frgrhash2wsp.v	$⊢ V = Vtx (G)$
	fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
Assertion	fusgr2wsp2nb	$⊢ (G \in FinUSGraph \land N \in V) \to M (N) = ⋃_{x \in G NeighbVtx N} ⋃_{y \in (G NeighbVtx N) ∖ \{x\}} \{⟨“ x N y ”⟩\}$

Proof

Step	Hyp	Ref	Expression
1		frgrhash2wsp.v	$⊢ V = Vtx (G)$
2		fusgreg2wsp.m	$⊢ M = (a \in V ⟼ \{w \in (2 WSPathsN G) \| w (1) = a\})$
3	1 2	fusgreg2wsplem	$⊢ N \in V \to (z \in M (N) \leftrightarrow (z \in (2 WSPathsN G) \land z (1) = N))$
4	3	adantl	$⊢ (G \in FinUSGraph \land N \in V) \to (z \in M (N) \leftrightarrow (z \in (2 WSPathsN G) \land z (1) = N))$
5	1	wspthsnwspthsnon	$⊢ z \in (2 WSPathsN G) \leftrightarrow \exists x \in V \exists y \in V z \in (x (2 WSPathsNOn G) y)$
6		fusgrusgr	$⊢ G \in FinUSGraph \to G \in USGraph$
7	6	adantr	$⊢ (G \in FinUSGraph \land N \in V) \to G \in USGraph$
8		eqid	$⊢ Edg (G) = Edg (G)$
9	1 8	usgr2wspthon	$⊢ (G \in USGraph \land (x \in V \land y \in V)) \to (z \in (x (2 WSPathsNOn G) y) \leftrightarrow \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
10	7 9	sylan	$⊢ ((G \in FinUSGraph \land N \in V) \land (x \in V \land y \in V)) \to (z \in (x (2 WSPathsNOn G) y) \leftrightarrow \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
11	10	2rexbidva	$⊢ (G \in FinUSGraph \land N \in V) \to (\exists x \in V \exists y \in V z \in (x (2 WSPathsNOn G) y) \leftrightarrow \exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
12	5 11	bitrid	$⊢ (G \in FinUSGraph \land N \in V) \to (z \in (2 WSPathsN G) \leftrightarrow \exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
13	12	anbi1d	$⊢ (G \in FinUSGraph \land N \in V) \to ((z \in (2 WSPathsN G) \land z (1) = N) \leftrightarrow (\exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \land z (1) = N))$
14		19.41vv	$⊢ \exists x \exists y (((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow (\exists x \exists y ((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N)$
15		velsn	$⊢ z \in \{⟨“ x N y ”⟩\} \leftrightarrow z = ⟨“ x N y ”⟩$
16	15	bicomi	$⊢ z = ⟨“ x N y ”⟩ \leftrightarrow z \in \{⟨“ x N y ”⟩\}$
17	16	anbi2i	$⊢ ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z \in \{⟨“ x N y ”⟩\})$
18	17	a1i	$⊢ (G \in FinUSGraph \land N \in V) \to (((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z \in \{⟨“ x N y ”⟩\}))$
19		simplr	$⊢ ((G \in FinUSGraph \land N \in V) \land ((x \in V \land y \in V) \land z (1) = N)) \to N \in V$
20		anass	$⊢ ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow (z = ⟨“ x m y ”⟩ \land (x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
21		ancom	$⊢ (z = ⟨“ x m y ”⟩ \land (x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \leftrightarrow ((x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \land z = ⟨“ x m y ”⟩)$
22		an12	$⊢ (x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow (\{x, m\} \in Edg (G) \land (x \neq y \land \{m, y\} \in Edg (G)))$
23		nesym	$⊢ x \neq y \leftrightarrow \neg y = x$
24		prcom	$⊢ \{m, y\} = \{y, m\}$
25	24	eleq1i	$⊢ \{m, y\} \in Edg (G) \leftrightarrow \{y, m\} \in Edg (G)$
26	23 25	anbi12ci	$⊢ (x \neq y \land \{m, y\} \in Edg (G)) \leftrightarrow (\{y, m\} \in Edg (G) \land \neg y = x)$
27	26	anbi2i	$⊢ (\{x, m\} \in Edg (G) \land (x \neq y \land \{m, y\} \in Edg (G))) \leftrightarrow (\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x))$
28	22 27	bitri	$⊢ (x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow (\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x))$
29	28	anbi1i	$⊢ ((x \neq y \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \land z = ⟨“ x m y ”⟩) \leftrightarrow ((\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x m y ”⟩)$
30	20 21 29	3bitri	$⊢ ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow ((\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x m y ”⟩)$
31		preq2	$⊢ m = N \to \{x, m\} = \{x, N\}$
32	31	eleq1d	$⊢ m = N \to (\{x, m\} \in Edg (G) \leftrightarrow \{x, N\} \in Edg (G))$
33		preq2	$⊢ m = N \to \{y, m\} = \{y, N\}$
34	33	eleq1d	$⊢ m = N \to (\{y, m\} \in Edg (G) \leftrightarrow \{y, N\} \in Edg (G))$
35	34	anbi1d	$⊢ m = N \to ((\{y, m\} \in Edg (G) \land \neg y = x) \leftrightarrow (\{y, N\} \in Edg (G) \land \neg y = x))$
36	32 35	anbi12d	$⊢ m = N \to ((\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x)) \leftrightarrow (\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)))$
37		s3eq2	$⊢ m = N \to ⟨“ x m y ”⟩ = ⟨“ x N y ”⟩$
38	37	eqeq2d	$⊢ m = N \to (z = ⟨“ x m y ”⟩ \leftrightarrow z = ⟨“ x N y ”⟩)$
39	36 38	anbi12d	$⊢ m = N \to (((\{x, m\} \in Edg (G) \land (\{y, m\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x m y ”⟩) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩))$
40	30 39	bitrid	$⊢ m = N \to (((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩))$
41	40	adantl	$⊢ (((G \in FinUSGraph \land N \in V) \land ((x \in V \land y \in V) \land z (1) = N)) \land m = N) \to (((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩))$
42		fveq1	$⊢ z = ⟨“ x m y ”⟩ \to z (1) = ⟨“ x m y ”⟩ (1)$
43		s3fv1	$⊢ m \in V \to ⟨“ x m y ”⟩ (1) = m$
44	43	elv	$⊢ ⟨“ x m y ”⟩ (1) = m$
45	42 44	eqtrdi	$⊢ z = ⟨“ x m y ”⟩ \to z (1) = m$
46	45	eqeq1d	$⊢ z = ⟨“ x m y ”⟩ \to (z (1) = N \leftrightarrow m = N)$
47	46	biimpd	$⊢ z = ⟨“ x m y ”⟩ \to (z (1) = N \to m = N)$
48	47	adantr	$⊢ (z = ⟨“ x m y ”⟩ \land x \neq y) \to (z (1) = N \to m = N)$
49	48	adantr	$⊢ ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \to (z (1) = N \to m = N)$
50	49	com12	$⊢ z (1) = N \to (((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \to m = N)$
51	50	ad2antll	$⊢ ((G \in FinUSGraph \land N \in V) \land ((x \in V \land y \in V) \land z (1) = N)) \to (((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \to m = N)$
52	51	imp	$⊢ (((G \in FinUSGraph \land N \in V) \land ((x \in V \land y \in V) \land z (1) = N)) \land ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \to m = N$
53	19 41 52	rspcebdv	$⊢ ((G \in FinUSGraph \land N \in V) \land ((x \in V \land y \in V) \land z (1) = N)) \to (\exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩))$
54	53	pm5.32da	$⊢ (G \in FinUSGraph \land N \in V) \to ((((x \in V \land y \in V) \land z (1) = N) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \leftrightarrow (((x \in V \land y \in V) \land z (1) = N) \land ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩)))$
55		an32	$⊢ (((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow (((x \in V \land y \in V) \land z (1) = N) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
56	55	a1i	$⊢ (G \in FinUSGraph \land N \in V) \to ((((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow (((x \in V \land y \in V) \land z (1) = N) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))))$
57		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
58	1 8	umgrpredgv	$⊢ (G \in UMGraph \land \{x, N\} \in Edg (G)) \to (x \in V \land N \in V)$
59	58	simpld	$⊢ (G \in UMGraph \land \{x, N\} \in Edg (G)) \to x \in V$
60	59	ex	$⊢ G \in UMGraph \to (\{x, N\} \in Edg (G) \to x \in V)$
61	1 8	umgrpredgv	$⊢ (G \in UMGraph \land \{y, N\} \in Edg (G)) \to (y \in V \land N \in V)$
62	61	simpld	$⊢ (G \in UMGraph \land \{y, N\} \in Edg (G)) \to y \in V$
63	62	expcom	$⊢ \{y, N\} \in Edg (G) \to (G \in UMGraph \to y \in V)$
64	63	adantr	$⊢ (\{y, N\} \in Edg (G) \land \neg y = x) \to (G \in UMGraph \to y \in V)$
65	64	com12	$⊢ G \in UMGraph \to ((\{y, N\} \in Edg (G) \land \neg y = x) \to y \in V)$
66	60 65	anim12d	$⊢ G \in UMGraph \to ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \to (x \in V \land y \in V))$
67	6 57 66	3syl	$⊢ G \in FinUSGraph \to ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \to (x \in V \land y \in V))$
68	67	adantr	$⊢ (G \in FinUSGraph \land N \in V) \to ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \to (x \in V \land y \in V))$
69	68	com12	$⊢ (\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \to ((G \in FinUSGraph \land N \in V) \to (x \in V \land y \in V))$
70	69	adantr	$⊢ ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \to ((G \in FinUSGraph \land N \in V) \to (x \in V \land y \in V))$
71	70	impcom	$⊢ ((G \in FinUSGraph \land N \in V) \land ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩)) \to (x \in V \land y \in V)$
72		fveq1	$⊢ z = ⟨“ x N y ”⟩ \to z (1) = ⟨“ x N y ”⟩ (1)$
73	72	adantl	$⊢ ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \to z (1) = ⟨“ x N y ”⟩ (1)$
74		s3fv1	$⊢ N \in V \to ⟨“ x N y ”⟩ (1) = N$
75	74	adantl	$⊢ (G \in FinUSGraph \land N \in V) \to ⟨“ x N y ”⟩ (1) = N$
76	73 75	sylan9eqr	$⊢ ((G \in FinUSGraph \land N \in V) \land ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩)) \to z (1) = N$
77	71 76	jca	$⊢ ((G \in FinUSGraph \land N \in V) \land ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩)) \to ((x \in V \land y \in V) \land z (1) = N)$
78	77	ex	$⊢ (G \in FinUSGraph \land N \in V) \to (((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \to ((x \in V \land y \in V) \land z (1) = N))$
79	78	pm4.71rd	$⊢ (G \in FinUSGraph \land N \in V) \to (((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩) \leftrightarrow (((x \in V \land y \in V) \land z (1) = N) \land ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩)))$
80	54 56 79	3bitr4d	$⊢ (G \in FinUSGraph \land N \in V) \to ((((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z = ⟨“ x N y ”⟩))$
81	8	nbusgreledg	$⊢ G \in USGraph \to (x \in (G NeighbVtx N) \leftrightarrow \{x, N\} \in Edg (G))$
82	6 81	syl	$⊢ G \in FinUSGraph \to (x \in (G NeighbVtx N) \leftrightarrow \{x, N\} \in Edg (G))$
83	82	adantr	$⊢ (G \in FinUSGraph \land N \in V) \to (x \in (G NeighbVtx N) \leftrightarrow \{x, N\} \in Edg (G))$
84		eldif	$⊢ y \in ((G NeighbVtx N) ∖ \{x\}) \leftrightarrow (y \in (G NeighbVtx N) \land \neg y \in \{x\})$
85	8	nbusgreledg	$⊢ G \in USGraph \to (y \in (G NeighbVtx N) \leftrightarrow \{y, N\} \in Edg (G))$
86	6 85	syl	$⊢ G \in FinUSGraph \to (y \in (G NeighbVtx N) \leftrightarrow \{y, N\} \in Edg (G))$
87	86	adantr	$⊢ (G \in FinUSGraph \land N \in V) \to (y \in (G NeighbVtx N) \leftrightarrow \{y, N\} \in Edg (G))$
88		velsn	$⊢ y \in \{x\} \leftrightarrow y = x$
89	88	a1i	$⊢ (G \in FinUSGraph \land N \in V) \to (y \in \{x\} \leftrightarrow y = x)$
90	89	notbid	$⊢ (G \in FinUSGraph \land N \in V) \to (\neg y \in \{x\} \leftrightarrow \neg y = x)$
91	87 90	anbi12d	$⊢ (G \in FinUSGraph \land N \in V) \to ((y \in (G NeighbVtx N) \land \neg y \in \{x\}) \leftrightarrow (\{y, N\} \in Edg (G) \land \neg y = x))$
92	84 91	bitrid	$⊢ (G \in FinUSGraph \land N \in V) \to (y \in ((G NeighbVtx N) ∖ \{x\}) \leftrightarrow (\{y, N\} \in Edg (G) \land \neg y = x))$
93	83 92	anbi12d	$⊢ (G \in FinUSGraph \land N \in V) \to ((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \leftrightarrow (\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)))$
94	93	anbi1d	$⊢ (G \in FinUSGraph \land N \in V) \to (((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \land z \in \{⟨“ x N y ”⟩\}) \leftrightarrow ((\{x, N\} \in Edg (G) \land (\{y, N\} \in Edg (G) \land \neg y = x)) \land z \in \{⟨“ x N y ”⟩\}))$
95	18 80 94	3bitr4d	$⊢ (G \in FinUSGraph \land N \in V) \to ((((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow ((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \land z \in \{⟨“ x N y ”⟩\}))$
96	95	2exbidv	$⊢ (G \in FinUSGraph \land N \in V) \to (\exists x \exists y (((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow \exists x \exists y ((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \land z \in \{⟨“ x N y ”⟩\}))$
97	14 96	bitr3id	$⊢ (G \in FinUSGraph \land N \in V) \to ((\exists x \exists y ((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N) \leftrightarrow \exists x \exists y ((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \land z \in \{⟨“ x N y ”⟩\}))$
98		r2ex	$⊢ \exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \leftrightarrow \exists x \exists y ((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))))$
99	98	anbi1i	$⊢ (\exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \land z (1) = N) \leftrightarrow (\exists x \exists y ((x \in V \land y \in V) \land \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G)))) \land z (1) = N)$
100		r2ex	$⊢ \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\} \leftrightarrow \exists x \exists y ((x \in (G NeighbVtx N) \land y \in ((G NeighbVtx N) ∖ \{x\})) \land z \in \{⟨“ x N y ”⟩\})$
101	97 99 100	3bitr4g	$⊢ (G \in FinUSGraph \land N \in V) \to ((\exists x \in V \exists y \in V \exists m \in V ((z = ⟨“ x m y ”⟩ \land x \neq y) \land (\{x, m\} \in Edg (G) \land \{m, y\} \in Edg (G))) \land z (1) = N) \leftrightarrow \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\})$
102		vex	$⊢ z \in V$
103		eleq1w	$⊢ p = z \to (p \in \{⟨“ x N y ”⟩\} \leftrightarrow z \in \{⟨“ x N y ”⟩\})$
104	103	2rexbidv	$⊢ p = z \to (\exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\} \leftrightarrow \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\})$
105	102 104	elab	$⊢ z \in \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\} \leftrightarrow \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\}$
106	105	bicomi	$⊢ \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\} \leftrightarrow z \in \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\}$
107	106	a1i	$⊢ (G \in FinUSGraph \land N \in V) \to (\exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) z \in \{⟨“ x N y ”⟩\} \leftrightarrow z \in \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\})$
108	13 101 107	3bitrd	$⊢ (G \in FinUSGraph \land N \in V) \to ((z \in (2 WSPathsN G) \land z (1) = N) \leftrightarrow z \in \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\})$
109	4 108	bitrd	$⊢ (G \in FinUSGraph \land N \in V) \to (z \in M (N) \leftrightarrow z \in \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\})$
110	109	eqrdv	$⊢ (G \in FinUSGraph \land N \in V) \to M (N) = \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\}$
111		dfiunv2	$⊢ ⋃_{x \in G NeighbVtx N} ⋃_{y \in (G NeighbVtx N) ∖ \{x\}} \{⟨“ x N y ”⟩\} = \{p \| \exists x \in (G NeighbVtx N) \exists y \in ((G NeighbVtx N) ∖ \{x\}) p \in \{⟨“ x N y ”⟩\}\}$
112	110 111	eqtr4di	$⊢ (G \in FinUSGraph \land N \in V) \to M (N) = ⋃_{x \in G NeighbVtx N} ⋃_{y \in (G NeighbVtx N) ∖ \{x\}} \{⟨“ x N y ”⟩\}$

Metamath Proof Explorer

Theorem fusgr2wsp2nb

Proof