Theorem el2spthonot 26397

Description: A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)

Assertion

Ref	Expression
el2spthonot	⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))

Distinct variable groups:   𝐴,𝑏,𝑓,𝑝   𝐶,𝑏,𝑓,𝑝   𝐸,𝑏,𝑓,𝑝   𝑇,𝑏,𝑓,𝑝   𝑉,𝑏,𝑓,𝑝   𝑋,𝑏,𝑓,𝑝   𝑌,𝑏,𝑓,𝑝

Proof of Theorem el2spthonot

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2spthonot 26393	. . . 4 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))})
2	1	eleq2d 2673	. . 3 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ 𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))}))
3		fveq2 6103	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → (1st ‘𝑡) = (1st ‘𝑇))
4	3	fveq2d 6107	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (1st ‘(1st ‘𝑡)) = (1st ‘(1st ‘𝑇)))
5	4	eqeq1d 2612	. . . . . . 7 ⊢ (𝑡 = 𝑇 → ((1st ‘(1st ‘𝑡)) = 𝐴 ↔ (1st ‘(1st ‘𝑇)) = 𝐴))
6	3	fveq2d 6107	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (2nd ‘(1st ‘𝑡)) = (2nd ‘(1st ‘𝑇)))
7	6	eqeq1d 2612	. . . . . . 7 ⊢ (𝑡 = 𝑇 → ((2nd ‘(1st ‘𝑡)) = (𝑝‘1) ↔ (2nd ‘(1st ‘𝑇)) = (𝑝‘1)))
8		fveq2 6103	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (2nd ‘𝑡) = (2nd ‘𝑇))
9	8	eqeq1d 2612	. . . . . . 7 ⊢ (𝑡 = 𝑇 → ((2nd ‘𝑡) = 𝐶 ↔ (2nd ‘𝑇) = 𝐶))
10	5, 7, 9	3anbi123d 1391	. . . . . 6 ⊢ (𝑡 = 𝑇 → (((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶) ↔ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))
11	10	3anbi3d 1397	. . . . 5 ⊢ (𝑡 = 𝑇 → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶)) ↔ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
12	11	2exbidv 1839	. . . 4 ⊢ (𝑡 = 𝑇 → (∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶)) ↔ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
13	12	elrab 3331	. . 3 ⊢ (𝑇 ∈ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐶))} ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
14	2, 13	syl6bb 275	. 2 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))))
15		vex 3176	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
16		vex 3176	. . . . . . . . . 10 ⊢ 𝑝 ∈ V
17	15, 16	pm3.2i 470	. . . . . . . . 9 ⊢ (𝑓 ∈ V ∧ 𝑝 ∈ V)
18		isspthon 26113	. . . . . . . . 9 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝)))
19	17, 18	mp3an2 1404	. . . . . . . 8 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝)))
20	19	3anbi1d 1395	. . . . . . 7 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
21	20	anbi2d 736	. . . . . 6 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))))
22		simpl 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑉)
23	22	ad2antll 761	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝐴 ∈ 𝑉)
24		spthispth 26103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → 𝑓(𝑉 Paths 𝐸)𝑝)
25		pthistrl 26102	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(𝑉 Paths 𝐸)𝑝 → 𝑓(𝑉 Trails 𝐸)𝑝)
26		trliswlk 26069	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(𝑉 Trails 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝)
27		el2wlkonotlem 26389	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (𝑝‘1) ∈ 𝑉)
28	27	ex 449	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(𝑉 Walks 𝐸)𝑝 → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉))
29	24, 25, 26, 28	4syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉))
30	29	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) → ((#‘𝑓) = 2 → (𝑝‘1) ∈ 𝑉))
31	30	imp 444	. . . . . . . . . . . . . . . 16 ⊢ (((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) → (𝑝‘1) ∈ 𝑉)
32	31	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (𝑝‘1) ∈ 𝑉)
33		simpr 476	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉)
34	33	ad2antll 761	. . . . . . . . . . . . . . 15 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝐶 ∈ 𝑉)
35		el2xptp0 7103	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑉 ∧ (𝑝‘1) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ 𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩))
36	23, 32, 34, 35	syl3anc 1318	. . . . . . . . . . . . . 14 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ 𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩))
37		oteq2 4350	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝‘1) = 𝑏 → ⟨𝐴, (𝑝‘1), 𝐶⟩ = ⟨𝐴, 𝑏, 𝐶⟩)
38	37	eqcoms 2618	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 = (𝑝‘1) → ⟨𝐴, (𝑝‘1), 𝐶⟩ = ⟨𝐴, 𝑏, 𝐶⟩)
39	38	eqeq2d 2620	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑝‘1) → (𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩ ↔ 𝑇 = ⟨𝐴, 𝑏, 𝐶⟩))
40	39	biimpd 218	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑝‘1) → (𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩ → 𝑇 = ⟨𝐴, 𝑏, 𝐶⟩))
41	40	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → (𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩ → 𝑇 = ⟨𝐴, 𝑏, 𝐶⟩))
42		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → 𝑓(𝑉 SPaths 𝐸)𝑝)
43	42	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → 𝑓(𝑉 SPaths 𝐸)𝑝)
44		simpllr 795	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → (#‘𝑓) = 2)
45		iswlkon 26062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑓 ∈ V ∧ 𝑝 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶)))
46	17, 45	mp3an2 1404	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶)))
47		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((#‘𝑓) = 2 → (𝑝‘(#‘𝑓)) = (𝑝‘2))
48	47	eqeq1d 2612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((#‘𝑓) = 2 → ((𝑝‘(#‘𝑓)) = 𝐶 ↔ (𝑝‘2) = 𝐶))
49	48	anbi2d 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑓) = 2 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) ↔ ((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶)))
50		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝‘0) = 𝐴 ↔ 𝐴 = (𝑝‘0))
51	50	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑝‘0) = 𝐴 → 𝐴 = (𝑝‘0))
52	51	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) → 𝐴 = (𝑝‘0))
53	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) ∧ 𝑏 = (𝑝‘1)) → 𝐴 = (𝑝‘0))
54		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) ∧ 𝑏 = (𝑝‘1)) → 𝑏 = (𝑝‘1))
55		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑝‘2) = 𝐶 ↔ 𝐶 = (𝑝‘2))
56	55	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑝‘2) = 𝐶 → 𝐶 = (𝑝‘2))
57	56	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) → 𝐶 = (𝑝‘2))
58	57	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) ∧ 𝑏 = (𝑝‘1)) → 𝐶 = (𝑝‘2))
59	53, 54, 58	3jca 1235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) ∧ 𝑏 = (𝑝‘1)) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))
60	59	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))
61	60	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((#‘𝑓) = 2 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘2) = 𝐶) → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
62	49, 61	sylbid 229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((#‘𝑓) = 2 → (((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
63	62	com12 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
64	63	3adant1 1072	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
65	64	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶) → ((#‘𝑓) = 2 → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
66	46, 65	sylbid 229	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 → ((#‘𝑓) = 2 → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
67	66	com3l 87	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 → ((#‘𝑓) = 2 → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
68	67	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) → ((#‘𝑓) = 2 → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑏 = (𝑝‘1) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
69	68	imp41 617	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))
70	43, 44, 69	3jca 1235	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))
71	41, 70	jctird 565	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) ∧ 𝑏 = (𝑝‘1)) → (𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩ → (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
72	32, 71	rspcimedv 3284	. . . . . . . . . . . . . 14 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → (𝑇 = ⟨𝐴, (𝑝‘1), 𝐶⟩ → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
73	36, 72	sylbid 229	. . . . . . . . . . . . 13 ⊢ ((((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
74	73	exp4b 630	. . . . . . . . . . . 12 ⊢ (((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))
75	74	com24 93	. . . . . . . . . . 11 ⊢ (((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2) → (((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))))
76	75	ex 449	. . . . . . . . . 10 ⊢ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) → ((#‘𝑓) = 2 → (((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))))))
77	76	3imp 1249	. . . . . . . . 9 ⊢ (((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))))
78	77	impcom 445	. . . . . . . 8 ⊢ ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
79	78	com12 32	. . . . . . 7 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) → ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
80	22	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝐴 ∈ 𝑉)
81		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
82	33	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝐶 ∈ 𝑉)
83	80, 81, 82	3jca 1235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
84		otel3xp 5077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
85	83, 84	sylan2 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉)) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
86	85	ex 449	. . . . . . . . . . . . . . 15 ⊢ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))
87	86	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))
88	87	com12 32	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝑏 ∈ 𝑉) → ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉)))
89	88	ex 449	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑏 ∈ 𝑉 → ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
90	89	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑏 ∈ 𝑉 → ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))))
91	90	imp31 447	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑇 ∈ ((𝑉 × 𝑉) × 𝑉))
92	24, 25, 26	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → 𝑓(𝑉 Walks 𝐸)𝑝)
93	92	3ad2ant1 1075	. . . . . . . . . . . . . 14 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(𝑉 Walks 𝐸)𝑝)
94	93	ad2antll 761	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑓(𝑉 Walks 𝐸)𝑝)
95		eqcom 2617	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 = (𝑝‘0) ↔ (𝑝‘0) = 𝐴)
96	95	biimpi 205	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = (𝑝‘0) → (𝑝‘0) = 𝐴)
97	96	3ad2ant1 1075	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘0) = 𝐴)
98	97	3ad2ant3 1077	. . . . . . . . . . . . . 14 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝‘0) = 𝐴)
99	98	ad2antll 761	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑝‘0) = 𝐴)
100		eqcom 2617	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐶 = (𝑝‘2) ↔ (𝑝‘2) = 𝐶)
101	100	biimpi 205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 = (𝑝‘2) → (𝑝‘2) = 𝐶)
102	101	3ad2ant3 1077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘2) = 𝐶)
103	102, 48	syl5ibr 235	. . . . . . . . . . . . . . . 16 ⊢ ((#‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘(#‘𝑓)) = 𝐶))
104	103	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → ((#‘𝑓) = 2 → ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑝‘(#‘𝑓)) = 𝐶)))
105	104	3imp 1249	. . . . . . . . . . . . . 14 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑝‘(#‘𝑓)) = 𝐶)
106	105	ad2antll 761	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑝‘(#‘𝑓)) = 𝐶)
107	46	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶)))
108	107	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ↔ (𝑓(𝑉 Walks 𝐸)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐶)))
109	94, 99, 106, 108	mpbir3and 1238	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝)
110		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑓(𝑉 SPaths 𝐸)𝑝 → 𝑓(𝑉 SPaths 𝐸)𝑝)
111	110	3ad2ant1 1075	. . . . . . . . . . . . 13 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → 𝑓(𝑉 SPaths 𝐸)𝑝)
112	111	ad2antll 761	. . . . . . . . . . . 12 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → 𝑓(𝑉 SPaths 𝐸)𝑝)
113	109, 112	jca 553	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝))
114		id 22	. . . . . . . . . . . . 13 ⊢ ((#‘𝑓) = 2 → (#‘𝑓) = 2)
115	114	3ad2ant2 1076	. . . . . . . . . . . 12 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (#‘𝑓) = 2)
116	115	ad2antll 761	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (#‘𝑓) = 2)
117	22	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐴 ∈ 𝑉)
118	117	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → 𝐴 ∈ 𝑉)
119		simpr 476	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → 𝑏 ∈ 𝑉)
120	33	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → 𝐶 ∈ 𝑉)
121	120	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → 𝐶 ∈ 𝑉)
122	118, 119, 121	3jca 1235	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉))
123		oteqimp 7078	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶)))
124	123	imp 444	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶))
125	122, 124	sylan2 490	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉)) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶))
126	125	ex 449	. . . . . . . . . . . . . . . 16 ⊢ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶)))
127		eqeq2 2621	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝‘1) = 𝑏 → ((2nd ‘(1st ‘𝑇)) = (𝑝‘1) ↔ (2nd ‘(1st ‘𝑇)) = 𝑏))
128	127	eqcoms 2618	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = (𝑝‘1) → ((2nd ‘(1st ‘𝑇)) = (𝑝‘1) ↔ (2nd ‘(1st ‘𝑇)) = 𝑏))
129	128	3anbi2d 1396	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = (𝑝‘1) → (((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶) ↔ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶)))
130	129	imbi2d 329	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = (𝑝‘1) → (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)) ↔ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = 𝑏 ∧ (2nd ‘𝑇) = 𝐶))))
131	126, 130	syl5ibr 235	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑝‘1) → (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
132	131	3ad2ant2 1076	. . . . . . . . . . . . . 14 ⊢ ((𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)) → (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
133	132	3ad2ant3 1077	. . . . . . . . . . . . 13 ⊢ ((𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))) → (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
134	133	impcom 445	. . . . . . . . . . . 12 ⊢ ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))
135	134	impcom 445	. . . . . . . . . . 11 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))
136	113, 116, 135	3jca 1235	. . . . . . . . . 10 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))
137	91, 136	jca 553	. . . . . . . . 9 ⊢ (((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) ∧ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
138	137	ex 449	. . . . . . . 8 ⊢ ((((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) ∧ 𝑏 ∈ 𝑉) → ((𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))))
139	138	rexlimdva 3013	. . . . . . 7 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) → (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶)))))
140	79, 139	impbid 201	. . . . . 6 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ((𝑓(𝐴(𝑉 WalkOn 𝐸)𝐶)𝑝 ∧ 𝑓(𝑉 SPaths 𝐸)𝑝) ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
141	21, 140	bitrd 267	. . . . 5 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
142	141	2exbidv 1839	. . . 4 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (∃𝑓∃𝑝(𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
143		19.42vv 1907	. . . 4 ⊢ (∃𝑓∃𝑝(𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ (𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ (𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))))
144		rexcom4 3198	. . . . 5 ⊢ (∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑓∃𝑏 ∈ 𝑉 ∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
145		rexcom4 3198	. . . . . 6 ⊢ (∃𝑏 ∈ 𝑉 ∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
146	145	exbii 1764	. . . . 5 ⊢ (∃𝑓∃𝑏 ∈ 𝑉 ∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
147	144, 146	bitr2i 264	. . . 4 ⊢ (∃𝑓∃𝑝∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
148	142, 143, 147	3bitr3g 301	. . 3 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
149		19.42vv 1907	. . . 4 ⊢ (∃𝑓∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
150	149	rexbii 3023	. . 3 ⊢ (∃𝑏 ∈ 𝑉 ∃𝑓∃𝑝(𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ (𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))
151	148, 150	syl6bb 275	. 2 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝑇 ∈ ((𝑉 × 𝑉) × 𝑉) ∧ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐶)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑇)) = 𝐴 ∧ (2nd ‘(1st ‘𝑇)) = (𝑝‘1) ∧ (2nd ‘𝑇) = 𝐶))) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))
152	14, 151	bitrd 267	1 ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = ⟨𝐴, 𝑏, 𝐶⟩ ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  {crab 2900  Vcvv 3173  ⟨cotp 4133   class class class wbr 4583   × cxp 5036  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058  0cc0 9815  1c1 9816  2c2 10947  #chash 12979   Walks cwalk 26026   Trails ctrail 26027   Paths cpath 26028   SPaths cspath 26029   WalkOn cwlkon 26030   SPathOn cspthon 26033   2SPathOnOt c2pthonot 26384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-ot 4134  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-wlk 26036  df-trail 26037  df-pth 26038  df-spth 26039  df-wlkon 26042  df-spthon 26045  df-2spthonot 26387

This theorem is referenced by:  el2spthonot0  26398  el2pthsot  26408  2spontn0vne  26414  2spotiundisj  26589