This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 }