elwspths2spth - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elwspths2spth		Structured version Visualization version GIF version

Theorem elwspths2spth 27852

Description: A simple path of length 2 between two vertices as length 3 string in a pseudograph. (Contributed by Alexander van der Vekens, 28-Feb-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 16-Mar-2022.)

**Hypothesis**
Ref	Expression
elwwlks2.v	⊢ 𝑉 = (Vtx‘𝐺)

**Assertion**
Ref	Expression
elwspths2spth	⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))

Distinct variable groups: 𝐺,𝑎,𝑏,𝑐,𝑓,𝑝 𝑉,𝑎,𝑏,𝑐,𝑓,𝑝 𝑊,𝑎,𝑏,𝑐,𝑓,𝑝

**Proof of Theorem elwspths2spth**
Step	Hyp	Ref	Expression
1		elwwlks2.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
2	1	wspthsnwspthsnon 27801	. . 3 ⊢ (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))
3	2	a1i 11	. 2 ⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))
4	1	elwspths2on 27845	. . . 4 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
5	4	3expb 1117	. . 3 ⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
6	5	2rexbidva 3223	. 2 ⊢ (𝐺 ∈ UPGraph → (∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
7		rexcom 3273	. . . 4 ⊢ (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))
8		wspthnon 27743	. . . . . . 7 ⊢ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩))
9		ancom 464	. . . . . . . . 9 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
10		19.41v 1950	. . . . . . . . 9 ⊢ (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
11	9, 10	bitr4i 281	. . . . . . . 8 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ ∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
12		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉)
13		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉)
14	12, 13	anim12i 615	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))
15		vex 3413	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
16		s3cli 14290	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V
17	15, 16	pm3.2i 474	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ V ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
18	1	isspthonpth 27637	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)))
19	14, 17, 18	sylancl 589	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)))
20		wwlknon 27742	. . . . . . . . . . . . 13 ⊢ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))
21		2nn0 11951	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
22		iswwlksn 27723	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℕ₀ → (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1))))
23	21, 22	mp1i 13	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1))))
24	23	3anbi1d 1437	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) ↔ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
25	20, 24	syl5bb 286	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
26	19, 25	anbi12d 633	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
27	26	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
28	16	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
29		simprl1 1215	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩)
30		spthiswlk 27616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ → 𝑓(Walks‘𝐺)⟨“𝑎𝑏𝑐”⟩)
31		wlklenvm1 27510	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(Walks‘𝐺)⟨“𝑎𝑏𝑐”⟩ → (♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1))
32		simpl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1))
33		oveq1 7157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = ((2 + 1) − 1))
34		2cn 11749	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
35		pncan1 11102	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 ∈ ℂ → ((2 + 1) − 1) = 2)
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 + 1) − 1) = 2
37	33, 36	eqtrdi 2809	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
38	37	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
39	38	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
40	39	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
41	32, 40	eqtrd 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = 2)
42	41	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
43	30, 31, 42	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
44	43	3ad2ant1 1130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
45	44	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = 2)
46	45	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (♯‘𝑓) = 2)
47		s3fv0 14300	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
48	47	elv 3415	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎
49	48	eqcomi 2767	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0)
50		s3fv1 14301	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏)
51	50	elv 3415	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏
52	51	eqcomi 2767	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1)
53		s3fv2 14302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)
54	53	elv 3415	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐
55	54	eqcomi 2767	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)
56	49, 52, 55	3pm3.2i 1336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))
57	56	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))
58	29, 46, 57	3jca 1125	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))))
59		breq2 5036	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑓(SPaths‘𝐺)𝑝 ↔ 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
60		fveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘0) = (⟨“𝑎𝑏𝑐”⟩‘0))
61	60	eqeq2d 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑎 = (𝑝‘0) ↔ 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0)))
62		fveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘1) = (⟨“𝑎𝑏𝑐”⟩‘1))
63	62	eqeq2d 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑏 = (𝑝‘1) ↔ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1)))
64		fveq1 6657	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘2) = (⟨“𝑎𝑏𝑐”⟩‘2))
65	64	eqeq2d 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑐 = (𝑝‘2) ↔ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))
66	61, 63, 65	3anbi123d 1433	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))))
67	59, 66	3anbi13d 1435	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))))
68	67	ad2antlr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))))
69	58, 68	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))
70	69	ex 416	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
71	28, 70	spcimedv 3512	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
72		spthiswlk 27616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝)
73		wlklenvp1 27507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1))
74		oveq1 7157	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = (2 + 1))
75		2p1e3 11816	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 + 1) = 3
76	74, 75	eqtrdi 2809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = 3)
77	76	eqeq2d 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔ (♯‘𝑝) = 3))
78	77	biimpcd 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
79	72, 73, 78	3syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(SPaths‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
80	79	imp 410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3)
81	80	3adant3 1129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑝) = 3)
82	81	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (♯‘𝑝) = 3)
83		eqcom 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎)
84		eqcom 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏)
85		eqcom 2765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐)
86	83, 84, 85	3anbi123i 1152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
87	86	biimpi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
88	87	3ad2ant3 1132	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
89	88	adantl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
90	82, 89	jca 515	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))
91	1	wlkpwrd 27506	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉)
92	72, 91	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉)
93	92	3ad2ant1 1130	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉)
94	12	anim1i 617	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)))
95		3anass 1092	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)))
96	94, 95	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))
97		eqwrds3 14372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))))
98	93, 96, 97	syl2anr 599	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))))
99	90, 98	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 = ⟨“𝑎𝑏𝑐”⟩)
100	59	biimpcd 252	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(SPaths‘𝐺)𝑝 → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
101	100	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
102	101	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
103	102	imp 410	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩)
104	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
105		fveq2 6658	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑓) = 2 → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = (⟨“𝑎𝑏𝑐”⟩‘2))
106	105, 54	eqtrdi 2809	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑓) = 2 → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
107	106	3ad2ant2 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
108	107	ad2antlr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
109	103, 104, 108	3jca 1125	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐))
110		wlkiswwlks1 27752	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
111	110	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
112	111	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
113	72, 112	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓(SPaths‘𝐺)𝑝 → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺)))
114	113	3ad2ant1 1130	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺)))
115	114	impcom 411	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 ∈ (WWalks‘𝐺))
116	115	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑝 ∈ (WWalks‘𝐺))
117		eleq1 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝 ∈ (WWalks‘𝐺) ↔ ⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺)))
118	117	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺)))
119	118	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺)))
120	116, 119	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺))
121		s3len 14303	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“𝑎𝑏𝑐”⟩) = 3
122		df-3 11738	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 = (2 + 1)
123	121, 122	eqtri 2781	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)
124	120, 123	jctir 524	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)))
125	54	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)
126	124, 104, 125	3jca 1125	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))
127	109, 126	jca 515	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
128	99, 127	mpdan 686	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
129	128	ex 416	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
130	129	exlimdv 1934	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
131	71, 130	impbid 215	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
132	131	adantr 484	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
133	27, 132	bitrd 282	. . . . . . . . 9 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
134	133	exbidv 1922	. . . . . . . 8 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
135	11, 134	syl5bb 286	. . . . . . 7 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
136	8, 135	syl5bb 286	. . . . . 6 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
137	136	pm5.32da 582	. . . . 5 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
138	137	2rexbidva 3223	. . . 4 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
139	7, 138	syl5bb 286	. . 3 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
140	139	rexbidva 3220	. 2 ⊢ (𝐺 ∈ UPGraph → (∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
141	3, 6, 140	3bitrd 308	1 ⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∃wrex 3071 Vcvv 3409 class class class wbr 5032 ‘cfv 6335 (class class class)co 7150 ℂcc 10573 0cc0 10575 1c1 10576 + caddc 10578 − cmin 10908 2c2 11729 3c3 11730 ℕ₀cn0 11934 ♯chash 13740 Word cword 13913 ⟨“cs3 14251 Vtxcvtx 26888 UPGraphcupgr 26972 Walkscwlks 27485 SPathscspths 27601 SPathsOncspthson 27603 WWalkscwwlks 27710 WWalksN cwwlksn 27711 WWalksNOn cwwlksnon 27712 WSPathsN cwwspthsn 27713 WSPathsNOn cwwspthsnon 27714

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5156 ax-sep 5169 ax-nul 5176 ax-pow 5234 ax-pr 5298 ax-un 7459 ax-ac2 9923 ax-cnex 10631 ax-resscn 10632 ax-1cn 10633 ax-icn 10634 ax-addcl 10635 ax-addrcl 10636 ax-mulcl 10637 ax-mulrcl 10638 ax-mulcom 10639 ax-addass 10640 ax-mulass 10641 ax-distr 10642 ax-i2m1 10643 ax-1ne0 10644 ax-1rid 10645 ax-rnegex 10646 ax-rrecex 10647 ax-cnre 10648 ax-pre-lttri 10649 ax-pre-lttrn 10650 ax-pre-ltadd 10651 ax-pre-mulgt0 10652

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ifp 1059 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3697 df-csb 3806 df-dif 3861 df-un 3863 df-in 3865 df-ss 3875 df-pss 3877 df-nul 4226 df-if 4421 df-pw 4496 df-sn 4523 df-pr 4525 df-tp 4527 df-op 4529 df-uni 4799 df-int 4839 df-iun 4885 df-br 5033 df-opab 5095 df-mpt 5113 df-tr 5139 df-id 5430 df-eprel 5435 df-po 5443 df-so 5444 df-fr 5483 df-se 5484 df-we 5485 df-xp 5530 df-rel 5531 df-cnv 5532 df-co 5533 df-dm 5534 df-rn 5535 df-res 5536 df-ima 5537 df-pred 6126 df-ord 6172 df-on 6173 df-lim 6174 df-suc 6175 df-iota 6294 df-fun 6337 df-fn 6338 df-f 6339 df-f1 6340 df-fo 6341 df-f1o 6342 df-fv 6343 df-isom 6344 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7580 df-1st 7693 df-2nd 7694 df-wrecs 7957 df-recs 8018 df-rdg 8056 df-1o 8112 df-2o 8113 df-oadd 8116 df-er 8299 df-map 8418 df-pm 8419 df-en 8528 df-dom 8529 df-sdom 8530 df-fin 8531 df-dju 9363 df-card 9401 df-ac 9576 df-pnf 10715 df-mnf 10716 df-xr 10717 df-ltxr 10718 df-le 10719 df-sub 10910 df-neg 10911 df-nn 11675 df-2 11737 df-3 11738 df-n0 11935 df-xnn0 12007 df-z 12021 df-uz 12283 df-fz 12940 df-fzo 13083 df-hash 13741 df-word 13914 df-concat 13970 df-s1 13997 df-s2 14257 df-s3 14258 df-edg 26940 df-uhgr 26950 df-upgr 26974 df-wlks 27488 df-wlkson 27489 df-trls 27581 df-trlson 27582 df-pths 27604 df-spths 27605 df-spthson 27607 df-wwlks 27715 df-wwlksn 27716 df-wwlksnon 27717 df-wspthsn 27718 df-wspthsnon 27719

This theorem is referenced by: (None)

W3C validator