wpthswwlks2on

Description: For two different vertices, a walk of length 2 between these vertices is a simple path of length 2 between these vertices in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018) (Revised by AV, 13-May-2021) (Revised by AV, 16-Mar-2022)

		Ref	Expression
	Assertion	wpthswwlks2on	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		wwlknon	⊢ ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) )
2	1	a1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
3	2	anbi1d	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
4		3anass	⊢ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
5	4	anbi1i	⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
6		anass	⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
7	5 6	bitri	⊢ ( ( ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
8	3 7	bitrdi	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∧ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) ) )
9	8	rabbidva2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } )
10		usgrupgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
11		wlklnwwlknupgr	⊢ ( 𝐺 ∈ UPGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) )
12	10 11	syl	⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ↔ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) )
13	12	bicomd	⊢ ( 𝐺 ∈ USGraph → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
14	13	adantr	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) ↔ ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
15		simprl	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( Walks ‘ 𝐺 ) 𝑤 )
16		simprl	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 )
17	16	adantr	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 0 ) = 𝐴 )
18		fveq2	⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) )
19	18	ad2antll	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = ( 𝑤 ‘ 2 ) )
20		simprr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 )
21	20	adantr	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ 2 ) = 𝐵 )
22	19 21	eqtrd	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 )
23		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
24	23	wlkp	⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
25		oveq2	⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 0 ... ( ♯ ‘ 𝑓 ) ) = ( 0 ... 2 ) )
26	25	feq2d	⊢ ( ( ♯ ‘ 𝑓 ) = 2 → ( 𝑤 : ( 0 ... ( ♯ ‘ 𝑓 ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
27	24 26	syl5ibcom	⊢ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 → ( ( ♯ ‘ 𝑓 ) = 2 → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) ) )
28	27	imp	⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) )
29		id	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) )
30		2nn0	⊢ 2 ∈ ℕ₀
31		0elfz	⊢ ( 2 ∈ ℕ₀ → 0 ∈ ( 0 ... 2 ) )
32	30 31	mp1i	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 0 ∈ ( 0 ... 2 ) )
33	29 32	ffvelrnd	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) )
34		nn0fz0	⊢ ( 2 ∈ ℕ₀ ↔ 2 ∈ ( 0 ... 2 ) )
35	30 34	mpbi	⊢ 2 ∈ ( 0 ... 2 )
36	35	a1i	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → 2 ∈ ( 0 ... 2 ) )
37	29 36	ffvelrnd	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) )
38	33 37	jca	⊢ ( 𝑤 : ( 0 ... 2 ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
39	28 38	syl	⊢ ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) )
40		eleq1	⊢ ( ( 𝑤 ‘ 0 ) = 𝐴 → ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) )
41		eleq1	⊢ ( ( 𝑤 ‘ 2 ) = 𝐵 → ( ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
42	40 41	bi2anan9	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑤 ‘ 2 ) ∈ ( Vtx ‘ 𝐺 ) ) ↔ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
43	39 42	syl5ib	⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
44	43	adantl	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ) )
45	44	imp	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
46		vex	⊢ 𝑓 ∈ V
47		vex	⊢ 𝑤 ∈ V
48	46 47	pm3.2i	⊢ ( 𝑓 ∈ V ∧ 𝑤 ∈ V )
49	23	iswlkon	⊢ ( ( ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ V ∧ 𝑤 ∈ V ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
50	45 48 49	sylancl	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ ( ♯ ‘ 𝑓 ) ) = 𝐵 ) ) )
51	15 17 22 50	mpbir3and	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
52		simplll	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐺 ∈ USGraph )
53		simprr	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( ♯ ‘ 𝑓 ) = 2 )
54		simpllr	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝐴 ≠ 𝐵 )
55		usgr2wlkspth	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝑓 ) = 2 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
56	52 53 54 55	syl3anc	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → ( 𝑓 ( 𝐴 ( WalksOn ‘ 𝐺 ) 𝐵 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
57	51 56	mpbid	⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) ∧ ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
58	57	ex	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
59	58	eximdv	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
60	59	ex	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
61	60	com23	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑓 ( 𝑓 ( Walks ‘ 𝐺 ) 𝑤 ∧ ( ♯ ‘ 𝑓 ) = 2 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
62	14 61	sylbid	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝑤 ∈ ( 2 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
63	62	imp	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) → ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
64	63	pm4.71d	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ↔ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ) )
65	64	bicomd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑤 ∈ ( 2 WWalksN 𝐺 ) ) → ( ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ) )
66	65	rabbidva	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) ∧ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } )
67	9 66	eqtrd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) } )
68	23	iswspthsnon	⊢ ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 }
69	23	iswwlksnon	⊢ ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 2 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 2 ) = 𝐵 ) }
70	67 68 69	3eqtr4g	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 ( 2 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 2 WWalksNOn 𝐺 ) 𝐵 ) )

Metamath Proof Explorer

Theorem wpthswwlks2on

Proof