Theorem iswspthsnon

Description: The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 12-May-2021) (Revised by AV, 14-Mar-2022)

	Ref	Expression
Hypothesis	iswspthsnon.v	|- V = ( Vtx ` G )
Assertion	iswspthsnon	|- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w }

Proof

Step	Hyp	Ref	Expression
1		iswspthsnon.v	|- V = ( Vtx ` G )
2		0ov	|- ( A (/) B ) = (/)
3		df-wspthsnon	|- WSPathsNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( a ( n WWalksNOn g ) b ) | E. f f ( a ( SPathsOn ` g ) b ) w } ) )
4	3	mpondm0	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( N WSPathsNOn G ) = (/) )
5	4	oveqd	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = ( A (/) B ) )
6		id	|- ( -. ( N e. NN0 /\ G e. _V ) -> -. ( N e. NN0 /\ G e. _V ) )
7	6	intnanrd	|- ( -. ( N e. NN0 /\ G e. _V ) -> -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) )
8	1	wwlksnon0	|- ( -. ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = (/) )
9	7 8	syl	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WWalksNOn G ) B ) = (/) )
10	9	rabeqdv	|- ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = { w e. (/) | E. f f ( A ( SPathsOn ` G ) B ) w } )
11		rab0	|- { w e. (/) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/)
12	10 11	eqtrdi	|- ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) )
13	2 5 12	3eqtr4a	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } )
14	1	wspthsnon	|- ( ( N e. NN0 /\ G e. _V ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) )
15	14	adantr	|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) )
16	15	oveqd	|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) )
17		eqid	|- ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } )
18	17	mpondm0	|- ( -. ( A e. V /\ B e. V ) -> ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) = (/) )
19	18	adantl	|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) B ) = (/) )
20	16 19	eqtrd	|- ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = (/) )
21	20	ex	|- ( ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) )
22	5 2	eqtrdi	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WSPathsNOn G ) B ) = (/) )
23	22	a1d	|- ( -. ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) ) )
24	21 23	pm2.61i	|- ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = (/) )
25	1	wwlksonvtx	|- ( w e. ( A ( N WWalksNOn G ) B ) -> ( A e. V /\ B e. V ) )
26	25	pm2.24d	|- ( w e. ( A ( N WWalksNOn G ) B ) -> ( -. ( A e. V /\ B e. V ) -> -. f ( A ( SPathsOn ` G ) B ) w ) )
27	26	impcom	|- ( ( -. ( A e. V /\ B e. V ) /\ w e. ( A ( N WWalksNOn G ) B ) ) -> -. f ( A ( SPathsOn ` G ) B ) w )
28	27	nexdv	|- ( ( -. ( A e. V /\ B e. V ) /\ w e. ( A ( N WWalksNOn G ) B ) ) -> -. E. f f ( A ( SPathsOn ` G ) B ) w )
29	28	ralrimiva	|- ( -. ( A e. V /\ B e. V ) -> A. w e. ( A ( N WWalksNOn G ) B ) -. E. f f ( A ( SPathsOn ` G ) B ) w )
30		rabeq0	|- ( { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) <-> A. w e. ( A ( N WWalksNOn G ) B ) -. E. f f ( A ( SPathsOn ` G ) B ) w )
31	29 30	sylibr	|- ( -. ( A e. V /\ B e. V ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } = (/) )
32	24 31	eqtr4d	|- ( -. ( A e. V /\ B e. V ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } )
33	14	adantr	|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( N WSPathsNOn G ) = ( a e. V , b e. V |-> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } ) )
34		oveq12	|- ( ( a = A /\ b = B ) -> ( a ( N WWalksNOn G ) b ) = ( A ( N WWalksNOn G ) B ) )
35		oveq12	|- ( ( a = A /\ b = B ) -> ( a ( SPathsOn ` G ) b ) = ( A ( SPathsOn ` G ) B ) )
36	35	breqd	|- ( ( a = A /\ b = B ) -> ( f ( a ( SPathsOn ` G ) b ) w <-> f ( A ( SPathsOn ` G ) B ) w ) )
37	36	exbidv	|- ( ( a = A /\ b = B ) -> ( E. f f ( a ( SPathsOn ` G ) b ) w <-> E. f f ( A ( SPathsOn ` G ) B ) w ) )
38	34 37	rabeqbidv	|- ( ( a = A /\ b = B ) -> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } )
39	38	adantl	|- ( ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) /\ ( a = A /\ b = B ) ) -> { w e. ( a ( N WWalksNOn G ) b ) | E. f f ( a ( SPathsOn ` G ) b ) w } = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } )
40		simprl	|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> A e. V )
41		simprr	|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> B e. V )
42		ovex	|- ( A ( N WWalksNOn G ) B ) e. _V
43	42	rabex	|- { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } e. _V
44	43	a1i	|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } e. _V )
45	33 39 40 41 44	ovmpod	|- ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w } )
46	13 32 45	ecase	|- ( A ( N WSPathsNOn G ) B ) = { w e. ( A ( N WWalksNOn G ) B ) | E. f f ( A ( SPathsOn ` G ) B ) w }