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 30559

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 30505	. . 3 ⊢ (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))
3	2	a1i 11	. 2 ⊢ (𝐺 ∈ UPGraph → (𝑊 ∈ (2 WSPathsN 𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))
4	1	elwspths2on 30551	. . . 4 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
5	4	3expb 1138	. . 3 ⊢ ((𝐺 ∈ UPGraph ∧ (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
6	5	2rexbidva 3226	. 2 ⊢ (𝐺 ∈ UPGraph → (∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 𝑊 ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑎 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐))))
7		rexcom 3292	. . . 4 ⊢ (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)))
8		wspthnon 30447	. . . . . . 7 ⊢ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩))
9		ancom 466	. . . . . . . . 9 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
10		19.41v 1982	. . . . . . . . 9 ⊢ (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ (∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
11	9, 10	bitr4i 281	. . . . . . . 8 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ ∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)))
12		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → 𝑎 ∈ 𝑉)
13		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → 𝑐 ∈ 𝑉)
14	12, 13	anim12i 625	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))
15		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
16		s3cli 15032	. . . . . . . . . . . . . 14 ⊢ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V
17	15, 16	pm3.2i 476	. . . . . . . . . . . . 13 ⊢ (𝑓 ∈ V ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
18	1	isspthonpth 30335	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ∧ (𝑓 ∈ V ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)))
19	14, 17, 18	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)))
20		wwlknon 30446	. . . . . . . . . . . . 13 ⊢ (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))
21		2nn0 12623	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
22		iswwlksn 30427	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℕ₀ → (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1))))
23	21, 22	mp1i 14	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ↔ (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1))))
24	23	3anbi1d 1468	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (2 WWalksN 𝐺) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) ↔ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
25	20, 24	bitrid 286	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ↔ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
26	19, 25	anbi12d 644	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
27	26	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
28	16	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ⟨“𝑎𝑏𝑐”⟩ ∈ Word V)
29		simprl1 1237	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩)
30		spthiswlk 30311	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ → 𝑓(Walks‘𝐺)⟨“𝑎𝑏𝑐”⟩)
31		wlklenvm1 30202	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(Walks‘𝐺)⟨“𝑎𝑏𝑐”⟩ → (♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1))
32		simpl 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1))
33		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = ((2 + 1) − 1))
34		2cn 12418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 2 ∈ ℂ
35		pncan1 11740	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (2 ∈ ℂ → ((2 + 1) − 1) = 2)
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((2 + 1) − 1) = 2
37	33, 36	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
38	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
39	38	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
40	39	adantl 487	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) = 2)
41	32, 40	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = 2)
42	41	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑓) = ((♯‘⟨“𝑎𝑏𝑐”⟩) − 1) → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
43	30, 31, 42	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
44	43	3ad2ant1 1151	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) → (((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐) → (♯‘𝑓) = 2))
45	44	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (♯‘𝑓) = 2)
46	45	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (♯‘𝑓) = 2)
47		s3fv0 15042	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
48	47	elv 3456	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎
49	48	eqcomi 2770	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0)
50		s3fv1 15043	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏)
51	50	elv 3456	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘1) = 𝑏
52	51	eqcomi 2770	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1)
53		s3fv2 15044	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ∈ V → (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)
54	53	elv 3456	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐
55	54	eqcomi 2770	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)
56	49, 52, 55	3pm3.2i 1358	. . . . . . . . . . . . . . . . 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 1146	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) ∧ ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))) → (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))))
59		breq2 5107	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑓(SPaths‘𝐺)𝑝 ↔ 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
60		fveq1 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘0) = (⟨“𝑎𝑏𝑐”⟩‘0))
61	60	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑎 = (𝑝‘0) ↔ 𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0)))
62		fveq1 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘1) = (⟨“𝑎𝑏𝑐”⟩‘1))
63	62	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑏 = (𝑝‘1) ↔ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1)))
64		fveq1 6884	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝‘2) = (⟨“𝑎𝑏𝑐”⟩‘2))
65	64	eqeq2d 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑐 = (𝑝‘2) ↔ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))
66	61, 63, 65	3anbi123d 1464	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2))))
67	59, 66	3anbi13d 1466	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) ↔ (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (⟨“𝑎𝑏𝑐”⟩‘0) ∧ 𝑏 = (⟨“𝑎𝑏𝑐”⟩‘1) ∧ 𝑐 = (⟨“𝑎𝑏𝑐”⟩‘2)))))
68	67	ad2antlr 740	. . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
71	28, 70	spcimedv 3550	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)) → ∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
72		spthiswlk 30311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑓(Walks‘𝐺)𝑝)
73		wlklenvp1 30199	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓(Walks‘𝐺)𝑝 → (♯‘𝑝) = ((♯‘𝑓) + 1))
74		oveq1 7427	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = (2 + 1))
75		2p1e3 12484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (2 + 1) = 3
76	74, 75	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑓) + 1) = 3)
77	76	eqeq2d 2772	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((♯‘𝑓) = 2 → ((♯‘𝑝) = ((♯‘𝑓) + 1) ↔ (♯‘𝑝) = 3))
78	77	biimpcd 252	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((♯‘𝑝) = ((♯‘𝑓) + 1) → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
79	72, 73, 78	3syl 19	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓(SPaths‘𝐺)𝑝 → ((♯‘𝑓) = 2 → (♯‘𝑝) = 3))
80	79	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2) → (♯‘𝑝) = 3)
81	80	3adant3 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (♯‘𝑝) = 3)
82	81	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (♯‘𝑝) = 3)
83		eqcom 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑝‘0) ↔ (𝑝‘0) = 𝑎)
84		eqcom 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 = (𝑝‘1) ↔ (𝑝‘1) = 𝑏)
85		eqcom 2768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑝‘2) ↔ (𝑝‘2) = 𝑐)
86	83, 84, 85	3anbi123i 1173	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) ↔ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
87	86	biimpi 219	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
88	87	3ad2ant3 1153	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
89	88	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))
90	82, 89	jca 521	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐)))
91	1	wlkpwrd 30198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉)
92	72, 91	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(SPaths‘𝐺)𝑝 → 𝑝 ∈ Word 𝑉)
93	92	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → 𝑝 ∈ Word 𝑉)
94	12	anim1i 627	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)))
95		3anass 1111	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) ↔ (𝑎 ∈ 𝑉 ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)))
96	94, 95	sylibr 237	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉))
97		eqwrds3 15114	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 ∈ Word 𝑉 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ ↔ ((♯‘𝑝) = 3 ∧ ((𝑝‘0) = 𝑎 ∧ (𝑝‘1) = 𝑏 ∧ (𝑝‘2) = 𝑐))))
98	93, 96, 97	syl2anr 609	. . . . . . . . . . . . . . . 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 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
102	101	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩))
103	102	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩)
104	48	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎)
105		fveq2 6885	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((♯‘𝑓) = 2 → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = (⟨“𝑎𝑏𝑐”⟩‘2))
106	105, 54	eqtrdi 2812	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝑓) = 2 → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
107	106	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
108	107	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐)
109	103, 104, 108	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐))
110		wlkiswwlks1 30456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐺 ∈ UPGraph → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
111	110	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
112	111	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → (𝑓(Walks‘𝐺)𝑝 → 𝑝 ∈ (WWalks‘𝐺)))
113	72, 112	syl5com 32	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓(SPaths‘𝐺)𝑝 → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺)))
114	113	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → 𝑝 ∈ (WWalks‘𝐺)))
115	114	impcom 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → 𝑝 ∈ (WWalks‘𝐺))
116	115	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → 𝑝 ∈ (WWalks‘𝐺))
117		eleq1 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (𝑝 ∈ (WWalks‘𝐺) ↔ ⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺)))
118	117	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = ⟨“𝑎𝑏𝑐”⟩ → (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺)))
119	118	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ↔ 𝑝 ∈ (WWalks‘𝐺)))
120	116, 119	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺))
121		s3len 15045	. . . . . . . . . . . . . . . . . . 19 ⊢ (♯‘⟨“𝑎𝑏𝑐”⟩) = 3
122		df-3 12406	. . . . . . . . . . . . . . . . . . 19 ⊢ 3 = (2 + 1)
123	121, 122	eqtri 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)
124	120, 123	jctir 530	. . . . . . . . . . . . . . . . 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 1146	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))
127	109, 126	jca 521	. . . . . . . . . . . . . . 15 ⊢ (((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) ∧ 𝑝 = ⟨“𝑎𝑏𝑐”⟩) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
128	99, 127	mpdan 700	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ (𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐)))
129	128	ex 418	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))) → ((𝑓(SPaths‘𝐺)⟨“𝑎𝑏𝑐”⟩ ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘(♯‘𝑓)) = 𝑐) ∧ ((⟨“𝑎𝑏𝑐”⟩ ∈ (WWalks‘𝐺) ∧ (♯‘⟨“𝑎𝑏𝑐”⟩) = (2 + 1)) ∧ (⟨“𝑎𝑏𝑐”⟩‘0) = 𝑎 ∧ (⟨“𝑎𝑏𝑐”⟩‘2) = 𝑐))))
130	129	exlimdv 1966	. . . . . . . . . . . 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 486	. . . . . . . . . 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 1954	. . . . . . . 8 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (∃𝑓(𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐)) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
135	11, 134	bitrid 286	. . . . . . 7 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → ((⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WWalksNOn 𝐺)𝑐) ∧ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑐)⟨“𝑎𝑏𝑐”⟩) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
136	8, 135	bitrid 286	. . . . . 6 ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) ∧ 𝑊 = ⟨“𝑎𝑏𝑐”⟩) → (⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐) ↔ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2)))))
137	136	pm5.32da 590	. . . . 5 ⊢ (((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉)) → ((𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
138	137	2rexbidva 3226	. . . 4 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
139	7, 138	bitrid 286	. . 3 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑐 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ⟨“𝑎𝑏𝑐”⟩ ∈ (𝑎(2 WSPathsNOn 𝐺)𝑐)) ↔ ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑊 = ⟨“𝑎𝑏𝑐”⟩ ∧ ∃𝑓∃𝑝(𝑓(SPaths‘𝐺)𝑝 ∧ (♯‘𝑓) = 2 ∧ (𝑎 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝑐 = (𝑝‘2))))))
140	139	rexbidva 3185	. 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

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ∃wrex 3087 Vcvv 3451 class class class wbr 5103 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 0cc0 11200 1c1 11201 + caddc 11203 − cmin 11541 2c2 12397 3c3 12398 ℕ₀cn0 12606 ♯chash 14474 Word cword 14658 ⟨“cs3 14993 Vtxcvtx 29574 UPGraphcupgr 29658 Walkscwlks 30177 SPathscspths 30296 SPathsOncspthson 30298 WWalkscwwlks 30414 WWalksN cwwlksn 30415 WWalksNOn cwwlksnon 30416 WSPathsN cwwspthsn 30417 WSPathsNOn cwwspthsnon 30418

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-ac2 10541 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-er 8717 df-map 8849 df-pm 8850 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-dju 9982 df-card 10020 df-ac 10195 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-xnn0 12680 df-z 12694 df-uz 12966 df-fz 13640 df-fzo 13789 df-hash 14475 df-word 14659 df-concat 14716 df-s1 14743 df-s2 14999 df-s3 15000 df-edg 29626 df-uhgr 29636 df-upgr 29660 df-wlks 30180 df-wlkson 30181 df-trls 30275 df-trlson 30276 df-pths 30299 df-spths 30300 df-spthson 30302 df-wwlks 30419 df-wwlksn 30420 df-wwlksnon 30421 df-wspthsn 30422 df-wspthsnon 30423

This theorem is used by: (None)

W3C validator