usgr2wlkneq

Description: The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 26-Jan-2021)

		Ref	Expression
	Assertion	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))$

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	upgriswlk	$⊢ G \in UPGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
5	1 4	syl	$⊢ G \in USGraph \to (F Walks (G) P \leftrightarrow (F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}))$
6		2wlklem	$⊢ \forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\})$
7		simplll	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to G \in USGraph$
8		fvex	$⊢ P (0) \in V$
9	3	usgrnloopv	$⊢ (G \in USGraph \land P (0) \in V) \to (iEdg (G) (F (0)) = \{P (0), P (1)\} \to P (0) \neq P (1))$
10	7 8 9	sylancl	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to (iEdg (G) (F (0)) = \{P (0), P (1)\} \to P (0) \neq P (1))$
11		fvex	$⊢ P (1) \in V$
12	3	usgrnloopv	$⊢ (G \in USGraph \land P (1) \in V) \to (iEdg (G) (F (1)) = \{P (1), P (2)\} \to P (1) \neq P (2))$
13	7 11 12	sylancl	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to (iEdg (G) (F (1)) = \{P (1), P (2)\} \to P (1) \neq P (2))$
14	10 13	anim12d	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to (P (0) \neq P (1) \land P (1) \neq P (2)))$
15		fveqeq2	$⊢ F (0) = F (1) \to (iEdg (G) (F (0)) = \{P (0), P (1)\} \leftrightarrow iEdg (G) (F (1)) = \{P (0), P (1)\})$
16		eqtr2	$⊢ (iEdg (G) (F (1)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to \{P (0), P (1)\} = \{P (1), P (2)\}$
17		prcom	$⊢ \{P (1), P (2)\} = \{P (2), P (1)\}$
18	17	eqeq2i	$⊢ \{P (0), P (1)\} = \{P (1), P (2)\} \leftrightarrow \{P (0), P (1)\} = \{P (2), P (1)\}$
19		fvex	$⊢ P (2) \in V$
20	8 19	preqr1	$⊢ \{P (0), P (1)\} = \{P (2), P (1)\} \to P (0) = P (2)$
21	18 20	sylbi	$⊢ \{P (0), P (1)\} = \{P (1), P (2)\} \to P (0) = P (2)$
22	16 21	syl	$⊢ (iEdg (G) (F (1)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) = P (2)$
23	22	ex	$⊢ iEdg (G) (F (1)) = \{P (0), P (1)\} \to (iEdg (G) (F (1)) = \{P (1), P (2)\} \to P (0) = P (2))$
24	15 23	syl6bi	$⊢ F (0) = F (1) \to (iEdg (G) (F (0)) = \{P (0), P (1)\} \to (iEdg (G) (F (1)) = \{P (1), P (2)\} \to P (0) = P (2)))$
25	24	impd	$⊢ F (0) = F (1) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to P (0) = P (2))$
26	25	com12	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to (F (0) = F (1) \to P (0) = P (2))$
27	26	necon3d	$⊢ (iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to (P (0) \neq P (2) \to F (0) \neq F (1))$
28	27	com12	$⊢ P (0) \neq P (2) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to F (0) \neq F (1))$
29	28	adantr	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to F (0) \neq F (1))$
30		simpl	$⊢ (P (0) \neq P (1) \land P (1) \neq P (2)) \to P (0) \neq P (1)$
31	30	adantl	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to P (0) \neq P (1)$
32		simpl	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to P (0) \neq P (2)$
33		simprr	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to P (1) \neq P (2)$
34	31 32 33	3jca	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to (P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2))$
35	29 34	jctild	$⊢ (P (0) \neq P (2) \land (P (0) \neq P (1) \land P (1) \neq P (2))) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))$
36	35	ex	$⊢ P (0) \neq P (2) \to ((P (0) \neq P (1) \land P (1) \neq P (2)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
37	36	com23	$⊢ P (0) \neq P (2) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (1) \neq P (2)) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
38	37	adantl	$⊢ ((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (1) \neq P (2)) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
39	38	adantr	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (1) \neq P (2)) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
40	14 39	mpdd	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to ((iEdg (G) (F (0)) = \{P (0), P (1)\} \land iEdg (G) (F (1)) = \{P (1), P (2)\}) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))$
41	6 40	syl5bi	$⊢ (((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \land P : (0 \dots 2) ⟶ Vtx (G)) \to (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))$
42	41	ex	$⊢ ((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \to (P : (0 \dots 2) ⟶ Vtx (G) \to (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
43	42	com23	$⊢ ((G \in USGraph \land F \in Word dom iEdg (G)) \land P (0) \neq P (2)) \to (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots 2) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
44	43	ex	$⊢ (G \in USGraph \land F \in Word dom iEdg (G)) \to (P (0) \neq P (2) \to (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots 2) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))))$
45		fveq2	$⊢ \|F\| = 2 \to P (\|F\|) = P (2)$
46	45	neeq2d	$⊢ \|F\| = 2 \to (P (0) \neq P (\|F\|) \leftrightarrow P (0) \neq P (2))$
47		oveq2	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = (0 ..^2)$
48		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
49	47 48	eqtrdi	$⊢ \|F\| = 2 \to (0 ..^\|F\|) = \{0, 1\}$
50	49	raleqdv	$⊢ \|F\| = 2 \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \leftrightarrow \forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\})$
51		oveq2	$⊢ \|F\| = 2 \to (0 \dots \|F\|) = (0 \dots 2)$
52	51	feq2d	$⊢ \|F\| = 2 \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \leftrightarrow P : (0 \dots 2) ⟶ Vtx (G))$
53	52	imbi1d	$⊢ \|F\| = 2 \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))) \leftrightarrow (P : (0 \dots 2) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))$
54	50 53	imbi12d	$⊢ \|F\| = 2 \to ((\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))) \leftrightarrow (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots 2) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))))$
55	46 54	imbi12d	$⊢ \|F\| = 2 \to ((P (0) \neq P (\|F\|) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))) \leftrightarrow (P (0) \neq P (2) \to (\forall k \in \{0, 1\} iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots 2) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))))$
56	44 55	syl5ibrcom	$⊢ (G \in USGraph \land F \in Word dom iEdg (G)) \to (\|F\| = 2 \to (P (0) \neq P (\|F\|) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1))))))$
57	56	impd	$⊢ (G \in USGraph \land F \in Word dom iEdg (G)) \to ((\|F\| = 2 \land P (0) \neq P (\|F\|)) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((P (0) \neq P (1) \land P (0) \neq P (2) \land P (1) \neq P (2)) \land F (0) \neq F (1)))))$
58	57	com24	$⊢ (G \in USGraph \land F \in Word dom iEdg (G)) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to ((\|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)))))$
59	58	ex	$⊢ G \in USGraph \to (F \in Word dom iEdg (G) \to (P : (0 \dots \|F\|) ⟶ Vtx (G) \to (\forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\} \to ((\|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))))))$
60	59	3impd	$⊢ G \in USGraph \to ((F \in Word dom iEdg (G) \land P : (0 \dots \|F\|) ⟶ Vtx (G) \land \forall k \in (0 ..^\|F\|) iEdg (G) (F (k)) = \{P (k), P (k + 1)\}) \to ((\|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))))$
61	5 60	sylbid	$⊢ G \in USGraph \to (F Walks (G) P \to ((\|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))))$
62	61	imp31	$⊢ ((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))$

Metamath Proof Explorer

Theorem usgr2wlkneq

Proof