upgrf1istrl

Description: Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 29-Oct-2021)

	Ref	Expression
Hypotheses	upgrtrls.v	$⊢ V = Vtx (G)$
	upgrtrls.i	$⊢ I = iEdg (G)$
Assertion	upgrf1istrl	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$

Proof

Step	Hyp	Ref	Expression
1		upgrtrls.v	$⊢ V = Vtx (G)$
2		upgrtrls.i	$⊢ I = iEdg (G)$
3	1 2	upgristrl	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow ((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
4		iswrdb	$⊢ F \in Word dom I \leftrightarrow F : (0 ..^\|F\|) ⟶ dom I$
5	4	a1i	$⊢ G \in UPGraph \to (F \in Word dom I \leftrightarrow F : (0 ..^\|F\|) ⟶ dom I)$
6	5	anbi1d	$⊢ G \in UPGraph \to ((F \in Word dom I \land Fun F^{-1}) \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1}))$
7		df-f1	$⊢ F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \leftrightarrow (F : (0 ..^\|F\|) ⟶ dom I \land Fun F^{-1})$
8	6 7	bitr4di	$⊢ G \in UPGraph \to ((F \in Word dom I \land Fun F^{-1}) \leftrightarrow F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I)$
9	8	3anbi1d	$⊢ G \in UPGraph \to (((F \in Word dom I \land Fun F^{-1}) \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
10	3 9	bitrd	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$

Metamath Proof Explorer

Theorem upgrf1istrl

Proof