Metamath Proof Explorer

Theorem numclwwlk1lem2f1o

Description: T is a 1-1 onto function. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 6-Mar-2022)

		Ref	Expression
	Hypotheses	extwwlkfab.v	$⊢ V = Vtx (G)$
		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
		numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
	Assertion	numclwwlk1lem2f1o	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{1-1 onto}{⟶} F \times (G NeighbVtx X)$

Proof

Step	Hyp	Ref	Expression
1		extwwlkfab.v	$⊢ V = Vtx (G)$
2		extwwlkfab.c	$⊢ C = (v \in V, n \in ℤ_{\geq 2} ⟼ \{w \in (v ClWWalksNOn (G) n) \| w (n - 2) = v\})$
3		extwwlkfab.f	$⊢ F = X ClWWalksNOn (G) (N - 2)$
4		numclwwlk.t	$⊢ T = (u \in (X C N) ⟼ ⟨u prefix (N - 2), u (N - 1)⟩)$
5	1 2 3 4	numclwwlk1lem2f1	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{1-1}{⟶} F \times (G NeighbVtx X)$
6	1 2 3 4	numclwwlk1lem2fo	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{onto}{⟶} F \times (G NeighbVtx X)$
7		df-f1o	$⊢ T : X C N \underset{1-1 onto}{⟶} F \times (G NeighbVtx X) \leftrightarrow (T : X C N \underset{1-1}{⟶} F \times (G NeighbVtx X) \land T : X C N \underset{onto}{⟶} F \times (G NeighbVtx X))$
8	5 6 7	sylanbrc	$⊢ (G \in USGraph \land X \in V \land N \in ℤ_{\geq 3}) \to T : X C N \underset{1-1 onto}{⟶} F \times (G NeighbVtx X)$