Metamath Proof Explorer

Theorem upgriseupth

Description: The property " <. F , P >. is an Eulerian path on the pseudograph G ". (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 3-May-2015) (Revised by AV, 18-Feb-2021) (Revised by AV, 30-Oct-2021)

		Ref	Expression
	Hypotheses	eupths.i	$⊢ I = iEdg (G)$
		upgriseupth.v	$⊢ V = Vtx (G)$
	Assertion	upgriseupth	$⊢ G \in UPGraph \to (F EulerPaths (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} 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		eupths.i	$⊢ I = iEdg (G)$
2		upgriseupth.v	$⊢ V = Vtx (G)$
3	1	iseupthf1o	$⊢ F EulerPaths (G) P \leftrightarrow (F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I)$
4	3	a1i	$⊢ G \in UPGraph \to (F EulerPaths (G) P \leftrightarrow (F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I))$
5	2 1	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
6	5	anbi1d	$⊢ G \in UPGraph \to ((F Walks (G) P \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \leftrightarrow ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I))$
7		simpr	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
8		simpl2	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \to P : (0 \dots \|F\|) ⟶ V$
9		simpl3	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \to \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}$
10	7 8 9	3jca	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \to (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
11		f1of	$⊢ F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to F : (0 ..^\|F\|) ⟶ dom I$
12		iswrdi	$⊢ F : (0 ..^\|F\|) ⟶ dom I \to F \in Word dom I$
13	11 12	syl	$⊢ F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \to F \in Word dom I$
14	13	3anim1i	$⊢ (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \to (F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
15		simp1	$⊢ (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \to F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I$
16	14 15	jca	$⊢ (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \to ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I)$
17	10 16	impbii	$⊢ ((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\})$
18	17	a1i	$⊢ G \in UPGraph \to (((F \in Word dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}) \land F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I) \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$
19	4 6 18	3bitrd	$⊢ G \in UPGraph \to (F EulerPaths (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1 onto}{⟶} dom I \land P : (0 \dots \|F\|) ⟶ V \land \forall k \in (0 ..^\|F\|) I (F (k)) = \{P (k), P (k + 1)\}))$