uhgrwkspthlem2

		Ref	Expression
	Assertion	uhgrwkspthlem2	$⊢ (F Walks (G) P \land (\|F\| = 1 \land A \neq B) \land (P (0) = A \land P (\|F\|) = B)) \to Fun P^{-1}$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2	1	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
3		oveq2	$⊢ \|F\| = 1 \to (0 \dots \|F\|) = (0 \dots 1)$
4		1e0p1	$⊢ 1 = 0 + 1$
5	4	oveq2i	$⊢ (0 \dots 1) = (0 \dots 0 + 1)$
6		0z	$⊢ 0 \in ℤ$
7		fzpr	$⊢ 0 \in ℤ \to (0 \dots 0 + 1) = \{0, 0 + 1\}$
8	6 7	ax-mp	$⊢ (0 \dots 0 + 1) = \{0, 0 + 1\}$
9		0p1e1	$⊢ 0 + 1 = 1$
10	9	preq2i	$⊢ \{0, 0 + 1\} = \{0, 1\}$
11	5 8 10	3eqtri	$⊢ (0 \dots 1) = \{0, 1\}$
12	3 11	eqtrdi	$⊢ \|F\| = 1 \to (0 \dots \|F\|) = \{0, 1\}$
13	12	feq2d	$⊢ \|F\| = 1 \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \leftrightarrow P : \{0, 1\} ⟶ Vtx (G))$
14	13	adantr	$⊢ (\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \leftrightarrow P : \{0, 1\} ⟶ Vtx (G))$
15		simpl	$⊢ (P (0) = A \land P (\|F\|) = B) \to P (0) = A$
16		simpr	$⊢ (P (0) = A \land P (\|F\|) = B) \to P (\|F\|) = B$
17	15 16	neeq12d	$⊢ (P (0) = A \land P (\|F\|) = B) \to (P (0) \neq P (\|F\|) \leftrightarrow A \neq B)$
18	17	bicomd	$⊢ (P (0) = A \land P (\|F\|) = B) \to (A \neq B \leftrightarrow P (0) \neq P (\|F\|))$
19		fveq2	$⊢ \|F\| = 1 \to P (\|F\|) = P (1)$
20	19	neeq2d	$⊢ \|F\| = 1 \to (P (0) \neq P (\|F\|) \leftrightarrow P (0) \neq P (1))$
21	18 20	sylan9bbr	$⊢ (\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to (A \neq B \leftrightarrow P (0) \neq P (1))$
22	14 21	anbi12d	$⊢ (\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land A \neq B) \leftrightarrow (P : \{0, 1\} ⟶ Vtx (G) \land P (0) \neq P (1)))$
23		1z	$⊢ 1 \in ℤ$
24		fpr2g	$⊢ (0 \in ℤ \land 1 \in ℤ) \to (P : \{0, 1\} ⟶ Vtx (G) \leftrightarrow (P (0) \in Vtx (G) \land P (1) \in Vtx (G) \land P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\}))$
25	6 23 24	mp2an	$⊢ P : \{0, 1\} ⟶ Vtx (G) \leftrightarrow (P (0) \in Vtx (G) \land P (1) \in Vtx (G) \land P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\})$
26		funcnvs2	$⊢ (P (0) \in Vtx (G) \land P (1) \in Vtx (G) \land P (0) \neq P (1)) \to Fun {⟨“ P (0) P (1) ”⟩}^{-1}$
27	26	3expa	$⊢ ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1)) \to Fun {⟨“ P (0) P (1) ”⟩}^{-1}$
28	27	adantl	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to Fun {⟨“ P (0) P (1) ”⟩}^{-1}$
29		simpl	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\}$
30		s2prop	$⊢ (P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \to ⟨“ P (0) P (1) ”⟩ = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\}$
31	30	eqcomd	$⊢ (P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \to \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} = ⟨“ P (0) P (1) ”⟩$
32	31	adantr	$⊢ ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1)) \to \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} = ⟨“ P (0) P (1) ”⟩$
33	32	adantl	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} = ⟨“ P (0) P (1) ”⟩$
34	29 33	eqtrd	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to P = ⟨“ P (0) P (1) ”⟩$
35	34	cnveqd	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to P^{-1} = {⟨“ P (0) P (1) ”⟩}^{-1}$
36	35	funeqd	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to (Fun P^{-1} \leftrightarrow Fun {⟨“ P (0) P (1) ”⟩}^{-1})$
37	28 36	mpbird	$⊢ (P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \land ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P (0) \neq P (1))) \to Fun P^{-1}$
38	37	exp32	$⊢ P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\} \to ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \to (P (0) \neq P (1) \to Fun P^{-1}))$
39	38	impcom	$⊢ ((P (0) \in Vtx (G) \land P (1) \in Vtx (G)) \land P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\}) \to (P (0) \neq P (1) \to Fun P^{-1})$
40	39	3impa	$⊢ (P (0) \in Vtx (G) \land P (1) \in Vtx (G) \land P = \{⟨0, P (0)⟩, ⟨1, P (1)⟩\}) \to (P (0) \neq P (1) \to Fun P^{-1})$
41	25 40	sylbi	$⊢ P : \{0, 1\} ⟶ Vtx (G) \to (P (0) \neq P (1) \to Fun P^{-1})$
42	41	imp	$⊢ (P : \{0, 1\} ⟶ Vtx (G) \land P (0) \neq P (1)) \to Fun P^{-1}$
43	22 42	syl6bi	$⊢ (\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land A \neq B) \to Fun P^{-1})$
44	43	expd	$⊢ (\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to (A \neq B \to Fun P^{-1}))$
45	44	com12	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((\|F\| = 1 \land (P (0) = A \land P (\|F\|) = B)) \to (A \neq B \to Fun P^{-1}))$
46	45	expd	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\|F\| = 1 \to ((P (0) = A \land P (\|F\|) = B) \to (A \neq B \to Fun P^{-1})))$
47	46	com34	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\|F\| = 1 \to (A \neq B \to ((P (0) = A \land P (\|F\|) = B) \to Fun P^{-1})))$
48	47	impd	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((\|F\| = 1 \land A \neq B) \to ((P (0) = A \land P (\|F\|) = B) \to Fun P^{-1}))$
49	2 48	syl	$⊢ F Walks (G) P \to ((\|F\| = 1 \land A \neq B) \to ((P (0) = A \land P (\|F\|) = B) \to Fun P^{-1}))$
50	49	3imp	$⊢ (F Walks (G) P \land (\|F\| = 1 \land A \neq B) \land (P (0) = A \land P (\|F\|) = B)) \to Fun P^{-1}$

Metamath Proof Explorer

Theorem uhgrwkspthlem2

Proof