wspthsnonn0vne

Description: If the set of simple paths of length at least 1 between two vertices is not empty, the two vertices must be different. (Contributed by Alexander van der Vekens, 3-Mar-2018) (Revised by AV, 16-May-2021)

		Ref	Expression
	Assertion	wspthsnonn0vne	$⊢ (N \in ℕ \land X (N WSPathsNOn G) Y \neq \emptyset) \to X \neq Y$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ X (N WSPathsNOn G) Y \neq \emptyset \leftrightarrow \exists p p \in (X (N WSPathsNOn G) Y)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3	2	wspthnonp	$⊢ p \in (X (N WSPathsNOn G) Y) \to ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G)) \land (p \in (X (N WWalksNOn G) Y) \land \exists f f (X SPathsOn (G) Y) p))$
4		wwlknon	$⊢ p \in (X (N WWalksNOn G) Y) \leftrightarrow (p \in (N WWalksN G) \land p (0) = X \land p (N) = Y)$
5		iswwlksn	$⊢ N \in ℕ_{0} \to (p \in (N WWalksN G) \leftrightarrow (p \in WWalks (G) \land \|p\| = N + 1))$
6		spthonisspth	$⊢ f (X SPathsOn (G) Y) p \to f SPaths (G) p$
7		spthispth	$⊢ f SPaths (G) p \to f Paths (G) p$
8		pthiswlk	$⊢ f Paths (G) p \to f Walks (G) p$
9		wlklenvm1	$⊢ f Walks (G) p \to \|f\| = \|p\| - 1$
10	8 9	syl	$⊢ f Paths (G) p \to \|f\| = \|p\| - 1$
11	6 7 10	3syl	$⊢ f (X SPathsOn (G) Y) p \to \|f\| = \|p\| - 1$
12		oveq1	$⊢ \|p\| = N + 1 \to \|p\| - 1 = N + 1 - 1$
13	12	eqeq2d	$⊢ \|p\| = N + 1 \to (\|f\| = \|p\| - 1 \leftrightarrow \|f\| = N + 1 - 1)$
14		simpr	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to \|f\| = N + 1 - 1$
15		nncn	$⊢ N \in ℕ \to N \in ℂ$
16		pncan1	$⊢ N \in ℂ \to N + 1 - 1 = N$
17	15 16	syl	$⊢ N \in ℕ \to N + 1 - 1 = N$
18	17	adantr	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to N + 1 - 1 = N$
19	14 18	eqtrd	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to \|f\| = N$
20		nnne0	$⊢ N \in ℕ \to N \neq 0$
21	20	adantr	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to N \neq 0$
22	19 21	eqnetrd	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to \|f\| \neq 0$
23		spthonepeq	$⊢ f (X SPathsOn (G) Y) p \to (X = Y \leftrightarrow \|f\| = 0)$
24	23	necon3bid	$⊢ f (X SPathsOn (G) Y) p \to (X \neq Y \leftrightarrow \|f\| \neq 0)$
25	22 24	syl5ibrcom	$⊢ (N \in ℕ \land \|f\| = N + 1 - 1) \to (f (X SPathsOn (G) Y) p \to X \neq Y)$
26	25	expcom	$⊢ \|f\| = N + 1 - 1 \to (N \in ℕ \to (f (X SPathsOn (G) Y) p \to X \neq Y))$
27	26	com23	$⊢ \|f\| = N + 1 - 1 \to (f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y))$
28	13 27	syl6bi	$⊢ \|p\| = N + 1 \to (\|f\| = \|p\| - 1 \to (f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
29	28	com13	$⊢ f (X SPathsOn (G) Y) p \to (\|f\| = \|p\| - 1 \to (\|p\| = N + 1 \to (N \in ℕ \to X \neq Y)))$
30	11 29	mpd	$⊢ f (X SPathsOn (G) Y) p \to (\|p\| = N + 1 \to (N \in ℕ \to X \neq Y))$
31	30	exlimiv	$⊢ \exists f f (X SPathsOn (G) Y) p \to (\|p\| = N + 1 \to (N \in ℕ \to X \neq Y))$
32	31	com12	$⊢ \|p\| = N + 1 \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y))$
33	32	adantl	$⊢ (p \in WWalks (G) \land \|p\| = N + 1) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y))$
34	5 33	syl6bi	$⊢ N \in ℕ_{0} \to (p \in (N WWalksN G) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
35	34	adantr	$⊢ (N \in ℕ_{0} \land G \in V) \to (p \in (N WWalksN G) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
36	35	adantr	$⊢ ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to (p \in (N WWalksN G) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
37	36	com12	$⊢ p \in (N WWalksN G) \to (((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
38	37	3ad2ant1	$⊢ (p \in (N WWalksN G) \land p (0) = X \land p (N) = Y) \to (((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
39	38	com12	$⊢ ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to ((p \in (N WWalksN G) \land p (0) = X \land p (N) = Y) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
40	4 39	biimtrid	$⊢ ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to (p \in (X (N WWalksNOn G) Y) \to (\exists f f (X SPathsOn (G) Y) p \to (N \in ℕ \to X \neq Y)))$
41	40	impd	$⊢ ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G))) \to ((p \in (X (N WWalksNOn G) Y) \land \exists f f (X SPathsOn (G) Y) p) \to (N \in ℕ \to X \neq Y))$
42	41	3impia	$⊢ ((N \in ℕ_{0} \land G \in V) \land (X \in Vtx (G) \land Y \in Vtx (G)) \land (p \in (X (N WWalksNOn G) Y) \land \exists f f (X SPathsOn (G) Y) p)) \to (N \in ℕ \to X \neq Y)$
43	3 42	syl	$⊢ p \in (X (N WSPathsNOn G) Y) \to (N \in ℕ \to X \neq Y)$
44	43	exlimiv	$⊢ \exists p p \in (X (N WSPathsNOn G) Y) \to (N \in ℕ \to X \neq Y)$
45	1 44	sylbi	$⊢ X (N WSPathsNOn G) Y \neq \emptyset \to (N \in ℕ \to X \neq Y)$
46	45	impcom	$⊢ (N \in ℕ \land X (N WSPathsNOn G) Y \neq \emptyset) \to X \neq Y$

Metamath Proof Explorer

Theorem wspthsnonn0vne

Proof