usgr2trlncl

Description: In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021) (Proof shortened by AV, 31-Oct-2021)

		Ref	Expression
	Assertion	usgr2trlncl	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Trails (G) P \to P (0) \neq P (2))$

Proof

Step	Hyp	Ref	Expression
1		usgrupgr	$⊢ G \in USGraph \to G \in UPGraph$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ iEdg (G) = iEdg (G)$
4	2 3	upgrf1istrl	$⊢ G \in UPGraph \to (F Trails (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}))$
5	1 4	syl	$⊢ G \in USGraph \to (F Trails (G) P \leftrightarrow (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}))$
6		eqidd	$⊢ \|F\| = 2 \to F = F$
7		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
8		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
9	7 8	eqtrdi	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = \{0, 1\}$
10		eqidd	$⊢ \|F\| = 2 \to dom iEdg (G) = dom iEdg (G)$
11	6 9 10	f1eq123d	$⊢ \|F\| = 2 \to (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \leftrightarrow F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G))$
12	9	raleqdv	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow \forall i \in \{0, 1\} iEdg (G) (F (i)) = \{P (i), P (i + 1)\})$
13		2wlklem	$⊢ \forall i \in \{0, 1\} iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})$
14	12 13	bitrdi	$⊢ \|F\| = 2 \to (\forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\} \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}))$
15	11 14	anbi12d	$⊢ \|F\| = 2 \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \leftrightarrow (F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})))$
16	15	adantl	$⊢ (G \in USGraph \land \|F\| = 2) \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \leftrightarrow (F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})))$
17		c0ex	$⊢ 0 \in V$
18		1ex	$⊢ 1 \in V$
19	17 18	pm3.2i	$⊢ (0 \in V \land 1 \in V)$
20		0ne1	$⊢ 0 \neq 1$
21		eqid	$⊢ \{0, 1\} = \{0, 1\}$
22	21	f12dfv	$⊢ ((0 \in V \land 1 \in V) \land 0 \neq 1) \to (F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \leftrightarrow (F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1)))$
23	19 20 22	mp2an	$⊢ F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \leftrightarrow (F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1))$
24		eqid	$⊢ Edg (G) = Edg (G)$
25	3 24	usgrf1oedg	$⊢ G \in USGraph \to iEdg (G) : dom iEdg (G) \underset{1-1 onto}{⟶} Edg (G)$
26		f1of1	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1 onto}{⟶} Edg (G) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)$
27		id	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to F : \{0, 1\} ⟶ dom iEdg (G)$
28	17	prid1	$⊢ 0 \in \{0, 1\}$
29	28	a1i	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to 0 \in \{0, 1\}$
30	27 29	ffvelrnd	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to F (0) \in dom iEdg (G)$
31	18	prid2	$⊢ 1 \in \{0, 1\}$
32	31	a1i	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to 1 \in \{0, 1\}$
33	27 32	ffvelrnd	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to F (1) \in dom iEdg (G)$
34	30 33	jca	$⊢ F : \{0, 1\} ⟶ dom iEdg (G) \to (F (0) \in dom iEdg (G) \land F (1) \in dom iEdg (G))$
35	34	anim1ci	$⊢ (F : \{0, 1\} ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)) \to (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G) \land (F (0) \in dom iEdg (G) \land F (1) \in dom iEdg (G)))$
36		f1veqaeq	$⊢ (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G) \land (F (0) \in dom iEdg (G) \land F (1) \in dom iEdg (G))) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to F (0) = F (1))$
37	35 36	syl	$⊢ (F : \{0, 1\} ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)) \to (iEdg (G) (F (0)) = iEdg (G) (F (1)) \to F (0) = F (1))$
38	37	necon3d	$⊢ (F : \{0, 1\} ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)) \to (F (0) \neq F (1) \to iEdg (G) (F (0)) \neq iEdg (G) (F (1)))$
39		simpl	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to iEdg (G) (F (0)) = \{P (0), P (1)\}$
40		simpr	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to iEdg (G) (F (1)) = \{P (1), P (2)\}$
41	39 40	neeq12d	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to (iEdg (G) (F (0)) \neq iEdg (G) (F (1)) \leftrightarrow \{P (0), P (1)\} \neq \{P (1), P (2)\})$
42		preq1	$⊢ P (0) = P (2) \to \{P (0), P (1)\} = \{P (2), P (1)\}$
43		prcom	$⊢ \{P (2), P (1)\} = \{P (1), P (2)\}$
44	42 43	eqtrdi	$⊢ P (0) = P (2) \to \{P (0), P (1)\} = \{P (1), P (2)\}$
45	44	necon3i	$⊢ \{P (0), P (1)\} \neq \{P (1), P (2)\} \to P (0) \neq P (2)$
46	41 45	syl6bi	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to (iEdg (G) (F (0)) \neq iEdg (G) (F (1)) \to P (0) \neq P (2))$
47	46	com12	$⊢ iEdg (G) (F (0)) \neq iEdg (G) (F (1)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))$
48	47	a1d	$⊢ iEdg (G) (F (0)) \neq iEdg (G) (F (1)) \to (G \in USGraph \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2)))$
49	38 48	syl6	$⊢ (F : \{0, 1\} ⟶ dom iEdg (G) \land iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G)) \to (F (0) \neq F (1) \to (G \in USGraph \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))))$
50	49	expcom	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G) \to (F : \{0, 1\} ⟶ dom iEdg (G) \to (F (0) \neq F (1) \to (G \in USGraph \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2)))))$
51	50	impd	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G) \to ((F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1)) \to (G \in USGraph \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))))$
52	51	com23	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} Edg (G) \to (G \in USGraph \to ((F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))))$
53	26 52	syl	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1 onto}{⟶} Edg (G) \to (G \in USGraph \to ((F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2))))$
54	25 53	mpcom	$⊢ G \in USGraph \to ((F : \{0, 1\} ⟶ dom iEdg (G) \land F (0) \neq F (1)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2)))$
55	23 54	syl5bi	$⊢ G \in USGraph \to (F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) \neq P (2)))$
56	55	impd	$⊢ G \in USGraph \to ((F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2))$
57	56	adantr	$⊢ (G \in USGraph \land \|F\| = 2) \to ((F : \{0, 1\} \underset{1-1}{⟶} dom iEdg (G) \land (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})) \to P (0) \neq P (2))$
58	16 57	sylbid	$⊢ (G \in USGraph \land \|F\| = 2) \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to P (0) \neq P (2))$
59	58	com12	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to P (0) \neq P (2))$
60	59	3adant2	$⊢ (F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to ((G \in USGraph \land \|F\| = 2) \to P (0) \neq P (2))$
61	60	expdcom	$⊢ G \in USGraph \to (\|F\| = 2 \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to P (0) \neq P (2)))$
62	61	com23	$⊢ G \in USGraph \to ((F : (0 ..^\|F\|) \underset{1-1}{⟶} dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall i \in (0 ..^\|F\|) iEdg (G) (F (i)) = \{P (i), P (i + 1)\}) \to (\|F\| = 2 \to P (0) \neq P (2)))$
63	5 62	sylbid	$⊢ G \in USGraph \to (F Trails (G) P \to (\|F\| = 2 \to P (0) \neq P (2)))$
64	63	com23	$⊢ G \in USGraph \to (\|F\| = 2 \to (F Trails (G) P \to P (0) \neq P (2)))$
65	64	imp	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Trails (G) P \to P (0) \neq P (2))$

Metamath Proof Explorer

Theorem usgr2trlncl

Proof