upgrwlkdvde

Description: In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk . (Contributed by AV, 17-Jan-2021)

		Ref	Expression
	Assertion	upgrwlkdvde	$⊢ (G \in UPGraph \land F Walks (G) P \land Fun P^{-1}) \to Fun F^{-1}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	1 2	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
4		df-f1	$⊢ P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \leftrightarrow (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun P^{-1})$
5	4	simplbi2	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (Fun P^{-1} \to P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G))$
6	5	3ad2ant2	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to (Fun P^{-1} \to P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G))$
7	6	impcom	$⊢ (Fun P^{-1} \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})) \to P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G)$
8		simpr1	$⊢ (Fun P^{-1} \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})) \to F \in Word dom iEdg (G)$
9	7 8	jca	$⊢ (Fun P^{-1} \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})) \to (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land F \in Word dom iEdg (G))$
10		simpr3	$⊢ (Fun P^{-1} \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})) \to \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}$
11		upgrwlkdvdelem	$⊢ (P : (0 \dots \|F\|) \underset{1-1}{⟶} Vtx (G) \land F \in Word dom iEdg (G)) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to Fun F^{-1})$
12	9 10 11	sylc	$⊢ (Fun P^{-1} \land (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\})) \to Fun F^{-1}$
13	12	expcom	$⊢ (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to (Fun P^{-1} \to Fun F^{-1})$
14	3 13	syl6bi	$⊢ G \in UPGraph \to (F Walks (G) P \to (Fun P^{-1} \to Fun F^{-1}))$
15	14	3imp	$⊢ (G \in UPGraph \land F Walks (G) P \land Fun P^{-1}) \to Fun F^{-1}$

Metamath Proof Explorer

Theorem upgrwlkdvde

Proof