wlkswwlksf1o

Description: The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021)

		Ref	Expression
	Hypothesis	wlkswwlksf1o.f	$⊢ F = (w \in Walks (G) ⟼ 2^{nd} (w))$
	Assertion	wlkswwlksf1o	$⊢ G \in USHGraph \to F : Walks (G) \underset{1-1 onto}{⟶} WWalks (G)$

Proof

Step	Hyp	Ref	Expression
1		wlkswwlksf1o.f	$⊢ F = (w \in Walks (G) ⟼ 2^{nd} (w))$
2		fvex	$⊢ 1^{st} (w) \in V$
3		breq1	$⊢ f = 1^{st} (w) \to (f Walks (G) 2^{nd} (w) \leftrightarrow 1^{st} (w) Walks (G) 2^{nd} (w))$
4	2 3	spcev	$⊢ 1^{st} (w) Walks (G) 2^{nd} (w) \to \exists f f Walks (G) 2^{nd} (w)$
5		wlkiswwlks	$⊢ G \in USHGraph \to (\exists f f Walks (G) 2^{nd} (w) \leftrightarrow 2^{nd} (w) \in WWalks (G))$
6	4 5	imbitrid	$⊢ G \in USHGraph \to (1^{st} (w) Walks (G) 2^{nd} (w) \to 2^{nd} (w) \in WWalks (G))$
7		wlkcpr	$⊢ w \in Walks (G) \leftrightarrow 1^{st} (w) Walks (G) 2^{nd} (w)$
8	7	biimpi	$⊢ w \in Walks (G) \to 1^{st} (w) Walks (G) 2^{nd} (w)$
9	6 8	impel	$⊢ (G \in USHGraph \land w \in Walks (G)) \to 2^{nd} (w) \in WWalks (G)$
10	9 1	fmptd	$⊢ G \in USHGraph \to F : Walks (G) ⟶ WWalks (G)$
11		simpr	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to F : Walks (G) ⟶ WWalks (G)$
12		fveq2	$⊢ w = x \to 2^{nd} (w) = 2^{nd} (x)$
13		id	$⊢ x \in Walks (G) \to x \in Walks (G)$
14		fvexd	$⊢ x \in Walks (G) \to 2^{nd} (x) \in V$
15	1 12 13 14	fvmptd3	$⊢ x \in Walks (G) \to F (x) = 2^{nd} (x)$
16		fveq2	$⊢ w = y \to 2^{nd} (w) = 2^{nd} (y)$
17		id	$⊢ y \in Walks (G) \to y \in Walks (G)$
18		fvexd	$⊢ y \in Walks (G) \to 2^{nd} (y) \in V$
19	1 16 17 18	fvmptd3	$⊢ y \in Walks (G) \to F (y) = 2^{nd} (y)$
20	15 19	eqeqan12d	$⊢ (x \in Walks (G) \land y \in Walks (G)) \to (F (x) = F (y) \leftrightarrow 2^{nd} (x) = 2^{nd} (y))$
21	20	adantl	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land (x \in Walks (G) \land y \in Walks (G))) \to (F (x) = F (y) \leftrightarrow 2^{nd} (x) = 2^{nd} (y))$
22		uspgr2wlkeqi	$⊢ (G \in USHGraph \land (x \in Walks (G) \land y \in Walks (G)) \land 2^{nd} (x) = 2^{nd} (y)) \to x = y$
23	22	ad4ant134	$⊢ (((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land (x \in Walks (G) \land y \in Walks (G))) \land 2^{nd} (x) = 2^{nd} (y)) \to x = y$
24	23	ex	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land (x \in Walks (G) \land y \in Walks (G))) \to (2^{nd} (x) = 2^{nd} (y) \to x = y)$
25	21 24	sylbid	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land (x \in Walks (G) \land y \in Walks (G))) \to (F (x) = F (y) \to x = y)$
26	25	ralrimivva	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to \forall x \in Walks (G) \forall y \in Walks (G) (F (x) = F (y) \to x = y)$
27		dff13	$⊢ F : Walks (G) \underset{1-1}{⟶} WWalks (G) \leftrightarrow (F : Walks (G) ⟶ WWalks (G) \land \forall x \in Walks (G) \forall y \in Walks (G) (F (x) = F (y) \to x = y))$
28	11 26 27	sylanbrc	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to F : Walks (G) \underset{1-1}{⟶} WWalks (G)$
29		wlkiswwlks	$⊢ G \in USHGraph \to (\exists f f Walks (G) y \leftrightarrow y \in WWalks (G))$
30	29	adantr	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to (\exists f f Walks (G) y \leftrightarrow y \in WWalks (G))$
31		df-br	$⊢ f Walks (G) y \leftrightarrow ⟨f, y⟩ \in Walks (G)$
32		vex	$⊢ f \in V$
33		vex	$⊢ y \in V$
34	32 33	op2nd	$⊢ 2^{nd} (⟨f, y⟩) = y$
35	34	eqcomi	$⊢ y = 2^{nd} (⟨f, y⟩)$
36		opex	$⊢ ⟨f, y⟩ \in V$
37		eleq1	$⊢ x = ⟨f, y⟩ \to (x \in Walks (G) \leftrightarrow ⟨f, y⟩ \in Walks (G))$
38		fveq2	$⊢ x = ⟨f, y⟩ \to 2^{nd} (x) = 2^{nd} (⟨f, y⟩)$
39	38	eqeq2d	$⊢ x = ⟨f, y⟩ \to (y = 2^{nd} (x) \leftrightarrow y = 2^{nd} (⟨f, y⟩))$
40	37 39	anbi12d	$⊢ x = ⟨f, y⟩ \to ((x \in Walks (G) \land y = 2^{nd} (x)) \leftrightarrow (⟨f, y⟩ \in Walks (G) \land y = 2^{nd} (⟨f, y⟩)))$
41	36 40	spcev	$⊢ (⟨f, y⟩ \in Walks (G) \land y = 2^{nd} (⟨f, y⟩)) \to \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
42	35 41	mpan2	$⊢ ⟨f, y⟩ \in Walks (G) \to \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
43	31 42	sylbi	$⊢ f Walks (G) y \to \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
44	43	exlimiv	$⊢ \exists f f Walks (G) y \to \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
45	30 44	syl6bir	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to (y \in WWalks (G) \to \exists x (x \in Walks (G) \land y = 2^{nd} (x)))$
46	45	imp	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land y \in WWalks (G)) \to \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
47		df-rex	$⊢ \exists x \in Walks (G) y = 2^{nd} (x) \leftrightarrow \exists x (x \in Walks (G) \land y = 2^{nd} (x))$
48	46 47	sylibr	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land y \in WWalks (G)) \to \exists x \in Walks (G) y = 2^{nd} (x)$
49	15	eqeq2d	$⊢ x \in Walks (G) \to (y = F (x) \leftrightarrow y = 2^{nd} (x))$
50	49	rexbiia	$⊢ \exists x \in Walks (G) y = F (x) \leftrightarrow \exists x \in Walks (G) y = 2^{nd} (x)$
51	48 50	sylibr	$⊢ ((G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \land y \in WWalks (G)) \to \exists x \in Walks (G) y = F (x)$
52	51	ralrimiva	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to \forall y \in WWalks (G) \exists x \in Walks (G) y = F (x)$
53		dffo3	$⊢ F : Walks (G) \underset{onto}{⟶} WWalks (G) \leftrightarrow (F : Walks (G) ⟶ WWalks (G) \land \forall y \in WWalks (G) \exists x \in Walks (G) y = F (x))$
54	11 52 53	sylanbrc	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to F : Walks (G) \underset{onto}{⟶} WWalks (G)$
55		df-f1o	$⊢ F : Walks (G) \underset{1-1 onto}{⟶} WWalks (G) \leftrightarrow (F : Walks (G) \underset{1-1}{⟶} WWalks (G) \land F : Walks (G) \underset{onto}{⟶} WWalks (G))$
56	28 54 55	sylanbrc	$⊢ (G \in USHGraph \land F : Walks (G) ⟶ WWalks (G)) \to F : Walks (G) \underset{1-1 onto}{⟶} WWalks (G)$
57	10 56	mpdan	$⊢ G \in USHGraph \to F : Walks (G) \underset{1-1 onto}{⟶} WWalks (G)$

Metamath Proof Explorer

Theorem wlkswwlksf1o

Proof