usgr2wlkspthlem2

		Ref	Expression
	Assertion	usgr2wlkspthlem2	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun P^{-1}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to G \in USGraph$
2	1	anim2i	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to (F Walks (G) P \land G \in USGraph)$
3	2	ancomd	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to (G \in USGraph \land F Walks (G) P)$
4		3simpc	$⊢ (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to (\|F\| = 2 \land P (0) \neq P (\|F\|))$
5	4	adantl	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to (\|F\| = 2 \land P (0) \neq P (\|F\|))$
6		usgr2wlkneq	$⊢ ((G \in USGraph \land F Walks (G) P) \land (\|F\| = 2 \land P (0) \neq P (\|F\|))) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))$
7	3 5 6	syl2anc	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))$
8		simpl	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to (P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2))$
9		fvex	$⊢ P (0) \in V$
10		fvex	$⊢ P (1) \in V$
11		fvex	$⊢ P (2) \in V$
12	9 10 11	3pm3.2i	$⊢ (P (0) \in V \land P (1) \in V \land P (2) \in V)$
13	8 12	jctil	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to ((P (0) \in V \land P (1) \in V \land P (2) \in V) \land (P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)))$
14		funcnvs3	$⊢ ((P (0) \in V \land P (1) \in V \land P (2) \in V) \land (P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2))) \to Fun {⟨“ P (0) P (1) P (2) ”⟩}^{-1}$
15	7 13 14	3syl	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun {⟨“ P (0) P (1) P (2) ”⟩}^{-1}$
16		eqid	$⊢ Vtx (G) = Vtx (G)$
17	16	wlkpwrd	$⊢ F Walks (G) P \to P \in Word Vtx (G)$
18		wlklenvp1	$⊢ F Walks (G) P \to \|P\| = \|F\| + 1$
19		oveq1	$⊢ \|F\| = 2 \to \|F\| + 1 = 2 + 1$
20		2p1e3	$⊢ 2 + 1 = 3$
21	19 20	eqtrdi	$⊢ \|F\| = 2 \to \|F\| + 1 = 3$
22	21	3ad2ant2	$⊢ (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to \|F\| + 1 = 3$
23	18 22	sylan9eq	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to \|P\| = 3$
24		wrdlen3s3	$⊢ (P \in Word Vtx (G) \land \|P\| = 3) \to P = ⟨“ P (0) P (1) P (2) ”⟩$
25	17 23 24	syl2an2r	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to P = ⟨“ P (0) P (1) P (2) ”⟩$
26	25	cnveqd	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to P^{-1} = {⟨“ P (0) P (1) P (2) ”⟩}^{-1}$
27	26	funeqd	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to (Fun P^{-1} \leftrightarrow Fun {⟨“ P (0) P (1) P (2) ”⟩}^{-1})$
28	15 27	mpbird	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun P^{-1}$

Metamath Proof Explorer

Theorem usgr2wlkspthlem2

Proof