Metamath Proof Explorer


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 }