pthdivtx

Description: The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

		Ref	Expression
	Assertion	pthdivtx	$⊢ (F Paths (G) P \land (I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J)) \to P (I) \neq P (J)$

Proof

Step	Hyp	Ref	Expression
1		ispth	$⊢ F Paths (G) P \leftrightarrow (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)$
2		trliswlk	$⊢ F Trails (G) P \to F Walks (G) P$
3		eqid	$⊢ Vtx (G) = Vtx (G)$
4	3	wlkp	$⊢ F Walks (G) P \to P : (0 \dots \|F\|) ⟶ Vtx (G)$
5		elfz0lmr	$⊢ J \in (0 \dots \|F\|) \to (J = 0 \lor J \in (1 ..^\|F\|) \lor J = \|F\|)$
6		elfzo1	$⊢ I \in (1 ..^\|F\|) \leftrightarrow (I \in ℕ \land \|F\| \in ℕ \land I < \|F\|)$
7		nnnn0	$⊢ \|F\| \in ℕ \to \|F\| \in ℕ_{0}$
8	7	3ad2ant2	$⊢ (I \in ℕ \land \|F\| \in ℕ \land I < \|F\|) \to \|F\| \in ℕ_{0}$
9	6 8	sylbi	$⊢ I \in (1 ..^\|F\|) \to \|F\| \in ℕ_{0}$
10	9	adantl	$⊢ (J = 0 \land I \in (1 ..^\|F\|)) \to \|F\| \in ℕ_{0}$
11		fvinim0ffz	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land \|F\| \in ℕ_{0}) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land P (\|F\|) \notin P [(1 ..^\|F\|)]))$
12	10 11	sylan2	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land P (\|F\|) \notin P [(1 ..^\|F\|)]))$
13		fveq2	$⊢ J = 0 \to P (J) = P (0)$
14	13	eqeq2d	$⊢ J = 0 \to (P (I) = P (J) \leftrightarrow P (I) = P (0))$
15	14	ad2antrl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \leftrightarrow P (I) = P (0))$
16		ffun	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to Fun P$
17	16	adantr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land I \in (1 ..^\|F\|)) \to Fun P$
18		fdm	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to dom P = (0 \dots \|F\|)$
19		fzo0ss1	$⊢ (1 ..^\|F\|) \subseteq (0 ..^\|F\|)$
20		fzossfz	$⊢ (0 ..^\|F\|) \subseteq (0 \dots \|F\|)$
21	19 20	sstri	$⊢ (1 ..^\|F\|) \subseteq (0 \dots \|F\|)$
22	21	sseli	$⊢ I \in (1 ..^\|F\|) \to I \in (0 \dots \|F\|)$
23		eleq2	$⊢ dom P = (0 \dots \|F\|) \to (I \in dom P \leftrightarrow I \in (0 \dots \|F\|))$
24	22 23	syl5ibr	$⊢ dom P = (0 \dots \|F\|) \to (I \in (1 ..^\|F\|) \to I \in dom P)$
25	18 24	syl	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (I \in (1 ..^\|F\|) \to I \in dom P)$
26	25	imp	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land I \in (1 ..^\|F\|)) \to I \in dom P$
27	17 26	jca	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land I \in (1 ..^\|F\|)) \to (Fun P \land I \in dom P)$
28	27	adantrl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (Fun P \land I \in dom P)$
29		simprr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to I \in (1 ..^\|F\|)$
30		funfvima	$⊢ (Fun P \land I \in dom P) \to (I \in (1 ..^\|F\|) \to P (I) \in P [(1 ..^\|F\|)])$
31	28 29 30	sylc	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to P (I) \in P [(1 ..^\|F\|)]$
32		eleq1	$⊢ P (I) = P (0) \to (P (I) \in P [(1 ..^\|F\|)] \leftrightarrow P (0) \in P [(1 ..^\|F\|)])$
33	31 32	syl5ibcom	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P (I) = P (0) \to P (0) \in P [(1 ..^\|F\|)])$
34	15 33	sylbid	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \to P (0) \in P [(1 ..^\|F\|)])$
35		nnel	$⊢ \neg P (0) \notin P [(1 ..^\|F\|)] \leftrightarrow P (0) \in P [(1 ..^\|F\|)]$
36	34 35	syl6ibr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \to \neg P (0) \notin P [(1 ..^\|F\|)])$
37	36	necon2ad	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P (0) \notin P [(1 ..^\|F\|)] \to P (I) \neq P (J))$
38	37	adantrd	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to ((P (0) \notin P [(1 ..^\|F\|)] \land P (\|F\|) \notin P [(1 ..^\|F\|)]) \to P (I) \neq P (J))$
39	12 38	sylbid	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = 0 \land I \in (1 ..^\|F\|))) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to P (I) \neq P (J))$
40	39	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((J = 0 \land I \in (1 ..^\|F\|)) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to P (I) \neq P (J)))$
41	40	com23	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((J = 0 \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J)))$
42	41	a1d	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((J = 0 \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J))))$
43	42	3imp	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to ((J = 0 \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J))$
44	43	com12	$⊢ (J = 0 \land I \in (1 ..^\|F\|)) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))$
45	44	a1d	$⊢ (J = 0 \land I \in (1 ..^\|F\|)) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J)))$
46	45	ex	$⊢ J = 0 \to (I \in (1 ..^\|F\|) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))))$
47		fvres	$⊢ I \in (1 ..^\|F\|) \to ({P ↾}_{(1 ..^\|F\|)}) (I) = P (I)$
48	47	adantl	$⊢ (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|)) \to ({P ↾}_{(1 ..^\|F\|)}) (I) = P (I)$
49	48	adantl	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to ({P ↾}_{(1 ..^\|F\|)}) (I) = P (I)$
50	49	eqcomd	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to P (I) = ({P ↾}_{(1 ..^\|F\|)}) (I)$
51		fvres	$⊢ J \in (1 ..^\|F\|) \to ({P ↾}_{(1 ..^\|F\|)}) (J) = P (J)$
52	51	ad2antrl	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to ({P ↾}_{(1 ..^\|F\|)}) (J) = P (J)$
53	52	eqcomd	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to P (J) = ({P ↾}_{(1 ..^\|F\|)}) (J)$
54	50 53	eqeq12d	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \leftrightarrow ({P ↾}_{(1 ..^\|F\|)}) (I) = ({P ↾}_{(1 ..^\|F\|)}) (J))$
55		fssres	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (1 ..^\|F\|) \subseteq (0 \dots \|F\|)) \to ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) ⟶ Vtx (G)$
56	21 55	mpan2	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) ⟶ Vtx (G)$
57		df-f1	$⊢ ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) \underset{1-1}{⟶} Vtx (G) \leftrightarrow (({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1})$
58	57	biimpri	$⊢ (({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \to ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) \underset{1-1}{⟶} Vtx (G)$
59	56 58	sylan	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1}) \to ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) \underset{1-1}{⟶} Vtx (G)$
60	59	3adant3	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to ({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) \underset{1-1}{⟶} Vtx (G)$
61		simpr	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))$
62	61	ancomd	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to (I \in (1 ..^\|F\|) \land J \in (1 ..^\|F\|))$
63		f1veqaeq	$⊢ (({P ↾}_{(1 ..^\|F\|)}) : (1 ..^\|F\|) \underset{1-1}{⟶} Vtx (G) \land (I \in (1 ..^\|F\|) \land J \in (1 ..^\|F\|))) \to (({P ↾}_{(1 ..^\|F\|)}) (I) = ({P ↾}_{(1 ..^\|F\|)}) (J) \to I = J)$
64	60 62 63	syl2an2r	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to (({P ↾}_{(1 ..^\|F\|)}) (I) = ({P ↾}_{(1 ..^\|F\|)}) (J) \to I = J)$
65	54 64	sylbid	$⊢ ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \land (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \to I = J)$
66	65	ancoms	$⊢ ((J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|)) \land (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)) \to (P (I) = P (J) \to I = J)$
67	66	necon3d	$⊢ ((J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|)) \land (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset)) \to (I \neq J \to P (I) \neq P (J))$
68	67	ex	$⊢ (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|)) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to (I \neq J \to P (I) \neq P (J)))$
69	68	com23	$⊢ (J \in (1 ..^\|F\|) \land I \in (1 ..^\|F\|)) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J)))$
70	69	ex	$⊢ J \in (1 ..^\|F\|) \to (I \in (1 ..^\|F\|) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))))$
71	9	adantl	$⊢ (J = \|F\| \land I \in (1 ..^\|F\|)) \to \|F\| \in ℕ_{0}$
72	71 11	sylan2	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \leftrightarrow (P (0) \notin P [(1 ..^\|F\|)] \land P (\|F\|) \notin P [(1 ..^\|F\|)]))$
73		fveq2	$⊢ J = \|F\| \to P (J) = P (\|F\|)$
74	73	eqeq2d	$⊢ J = \|F\| \to (P (I) = P (J) \leftrightarrow P (I) = P (\|F\|))$
75	74	ad2antrl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \leftrightarrow P (I) = P (\|F\|))$
76	27	adantrl	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (Fun P \land I \in dom P)$
77		simprr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to I \in (1 ..^\|F\|)$
78	76 77 30	sylc	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to P (I) \in P [(1 ..^\|F\|)]$
79		eleq1	$⊢ P (I) = P (\|F\|) \to (P (I) \in P [(1 ..^\|F\|)] \leftrightarrow P (\|F\|) \in P [(1 ..^\|F\|)])$
80	78 79	syl5ibcom	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P (I) = P (\|F\|) \to P (\|F\|) \in P [(1 ..^\|F\|)])$
81	75 80	sylbid	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \to P (\|F\|) \in P [(1 ..^\|F\|)])$
82		nnel	$⊢ \neg P (\|F\|) \notin P [(1 ..^\|F\|)] \leftrightarrow P (\|F\|) \in P [(1 ..^\|F\|)]$
83	81 82	syl6ibr	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P (I) = P (J) \to \neg P (\|F\|) \notin P [(1 ..^\|F\|)])$
84	83	necon2ad	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P (\|F\|) \notin P [(1 ..^\|F\|)] \to P (I) \neq P (J))$
85	84	adantld	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to ((P (0) \notin P [(1 ..^\|F\|)] \land P (\|F\|) \notin P [(1 ..^\|F\|)]) \to P (I) \neq P (J))$
86	72 85	sylbid	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land (J = \|F\| \land I \in (1 ..^\|F\|))) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to P (I) \neq P (J))$
87	86	ex	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to ((J = \|F\| \land I \in (1 ..^\|F\|)) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to P (I) \neq P (J)))$
88	87	com23	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((J = \|F\| \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J)))$
89	88	a1d	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((J = \|F\| \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J))))$
90	89	3imp	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to ((J = \|F\| \land I \in (1 ..^\|F\|)) \to P (I) \neq P (J))$
91	90	com12	$⊢ (J = \|F\| \land I \in (1 ..^\|F\|)) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))$
92	91	a1d	$⊢ (J = \|F\| \land I \in (1 ..^\|F\|)) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J)))$
93	92	ex	$⊢ J = \|F\| \to (I \in (1 ..^\|F\|) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))))$
94	46 70 93	3jaoi	$⊢ (J = 0 \lor J \in (1 ..^\|F\|) \lor J = \|F\|) \to (I \in (1 ..^\|F\|) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))))$
95	5 94	syl	$⊢ J \in (0 \dots \|F\|) \to (I \in (1 ..^\|F\|) \to (I \neq J \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))))$
96	95	3imp21	$⊢ (I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to ((P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to P (I) \neq P (J))$
97	96	com12	$⊢ (P : (0 \dots \|F\|) ⟶ Vtx (G) \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to ((I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to P (I) \neq P (J))$
98	97	3exp	$⊢ P : (0 \dots \|F\|) ⟶ Vtx (G) \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to P (I) \neq P (J))))$
99	2 4 98	3syl	$⊢ F Trails (G) P \to (Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \to (P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset \to ((I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to P (I) \neq P (J))))$
100	99	3imp	$⊢ (F Trails (G) P \land Fun {({P ↾}_{(1 ..^\|F\|)})}^{-1} \land P [\{0, \|F\|\}] \cap P [(1 ..^\|F\|)] = \emptyset) \to ((I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to P (I) \neq P (J))$
101	1 100	sylbi	$⊢ F Paths (G) P \to ((I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J) \to P (I) \neq P (J))$
102	101	imp	$⊢ (F Paths (G) P \land (I \in (1 ..^\|F\|) \land J \in (0 \dots \|F\|) \land I \neq J)) \to P (I) \neq P (J)$

Metamath Proof Explorer

Theorem pthdivtx

Proof