usgr2wlkspthlem1

		Ref	Expression
	Assertion	usgr2wlkspthlem1	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun F^{-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		fvexd	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to F (0) \in V$
9		fvexd	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to F (1) \in V$
10		simpr	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to F (0) \neq F (1)$
11	8 9 10	3jca	$⊢ ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)) \to (F (0) \in V \land F (1) \in V \land F (0) \neq F (1))$
12		funcnvs2	$⊢ (F (0) \in V \land F (1) \in V \land F (0) \neq F (1)) \to Fun {⟨“ F (0) F (1) ”⟩}^{-1}$
13	7 11 12	3syl	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun {⟨“ F (0) F (1) ”⟩}^{-1}$
14		eqid	$⊢ iEdg (G) = iEdg (G)$
15	14	wlkf	$⊢ F Walks (G) P \to F \in Word dom iEdg (G)$
16		simp2	$⊢ (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|)) \to \|F\| = 2$
17		wrdlen2s2	$⊢ (F \in Word dom iEdg (G) \land \|F\| = 2) \to F = ⟨“ F (0) F (1) ”⟩$
18	15 16 17	syl2an	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to F = ⟨“ F (0) F (1) ”⟩$
19	18	cnveqd	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to F^{-1} = {⟨“ F (0) F (1) ”⟩}^{-1}$
20	19	funeqd	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to (Fun F^{-1} \leftrightarrow Fun {⟨“ F (0) F (1) ”⟩}^{-1})$
21	13 20	mpbird	$⊢ (F Walks (G) P \land (G \in USGraph \land \|F\| = 2 \land P (0) \neq P (\|F\|))) \to Fun F^{-1}$

Metamath Proof Explorer

Theorem usgr2wlkspthlem1

Proof