Metamath Proof Explorer


Theorem iswwlksnon

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

Ref Expression
Hypothesis iswwlksnon.v
|- V = ( Vtx ` G )
Assertion iswwlksnon
|- ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) }

Proof

Step Hyp Ref Expression
1 iswwlksnon.v
 |-  V = ( Vtx ` G )
2 0ov
 |-  ( A (/) B ) = (/)
3 df-wwlksnon
 |-  WWalksNOn = ( n e. NN0 , g e. _V |-> ( a e. ( Vtx ` g ) , b e. ( Vtx ` g ) |-> { w e. ( n WWalksN g ) | ( ( w ` 0 ) = a /\ ( w ` n ) = b ) } ) )
4 3 mpondm0
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N WWalksNOn G ) = (/) )
5 4 oveqd
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WWalksNOn G ) B ) = ( A (/) B ) )
6 df-wwlksn
 |-  WWalksN = ( n e. NN0 , g e. _V |-> { w e. ( WWalks ` g ) | ( # ` w ) = ( n + 1 ) } )
7 6 mpondm0
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( N WWalksN G ) = (/) )
8 7 rabeqdv
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } = { w e. (/) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
9 rab0
 |-  { w e. (/) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } = (/)
10 8 9 eqtrdi
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } = (/) )
11 2 5 10 3eqtr4a
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
12 1 wwlksnon
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
13 12 adantr
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
14 13 oveqd
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = ( A ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) B ) )
15 eqid
 |-  ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } )
16 15 mpondm0
 |-  ( -. ( A e. V /\ B e. V ) -> ( A ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) B ) = (/) )
17 16 adantl
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) B ) = (/) )
18 14 17 eqtrd
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ -. ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = (/) )
19 18 ex
 |-  ( ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WWalksNOn G ) B ) = (/) ) )
20 5 2 eqtrdi
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( A ( N WWalksNOn G ) B ) = (/) )
21 20 a1d
 |-  ( -. ( N e. NN0 /\ G e. _V ) -> ( -. ( A e. V /\ B e. V ) -> ( A ( N WWalksNOn G ) B ) = (/) ) )
22 19 21 pm2.61i
 |-  ( -. ( A e. V /\ B e. V ) -> ( A ( N WWalksNOn G ) B ) = (/) )
23 1 wwlknllvtx
 |-  ( w e. ( N WWalksN G ) -> ( ( w ` 0 ) e. V /\ ( w ` N ) e. V ) )
24 eleq1
 |-  ( A = ( w ` 0 ) -> ( A e. V <-> ( w ` 0 ) e. V ) )
25 24 eqcoms
 |-  ( ( w ` 0 ) = A -> ( A e. V <-> ( w ` 0 ) e. V ) )
26 eleq1
 |-  ( B = ( w ` N ) -> ( B e. V <-> ( w ` N ) e. V ) )
27 26 eqcoms
 |-  ( ( w ` N ) = B -> ( B e. V <-> ( w ` N ) e. V ) )
28 25 27 bi2anan9
 |-  ( ( ( w ` 0 ) = A /\ ( w ` N ) = B ) -> ( ( A e. V /\ B e. V ) <-> ( ( w ` 0 ) e. V /\ ( w ` N ) e. V ) ) )
29 23 28 syl5ibrcom
 |-  ( w e. ( N WWalksN G ) -> ( ( ( w ` 0 ) = A /\ ( w ` N ) = B ) -> ( A e. V /\ B e. V ) ) )
30 29 con3rr3
 |-  ( -. ( A e. V /\ B e. V ) -> ( w e. ( N WWalksN G ) -> -. ( ( w ` 0 ) = A /\ ( w ` N ) = B ) ) )
31 30 ralrimiv
 |-  ( -. ( A e. V /\ B e. V ) -> A. w e. ( N WWalksN G ) -. ( ( w ` 0 ) = A /\ ( w ` N ) = B ) )
32 rabeq0
 |-  ( { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } = (/) <-> A. w e. ( N WWalksN G ) -. ( ( w ` 0 ) = A /\ ( w ` N ) = B ) )
33 31 32 sylibr
 |-  ( -. ( A e. V /\ B e. V ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } = (/) )
34 22 33 eqtr4d
 |-  ( -. ( A e. V /\ B e. V ) -> ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
35 12 adantr
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( N WWalksNOn G ) = ( a e. V , b e. V |-> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } ) )
36 eqeq2
 |-  ( a = A -> ( ( w ` 0 ) = a <-> ( w ` 0 ) = A ) )
37 eqeq2
 |-  ( b = B -> ( ( w ` N ) = b <-> ( w ` N ) = B ) )
38 36 37 bi2anan9
 |-  ( ( a = A /\ b = B ) -> ( ( ( w ` 0 ) = a /\ ( w ` N ) = b ) <-> ( ( w ` 0 ) = A /\ ( w ` N ) = B ) ) )
39 38 rabbidv
 |-  ( ( a = A /\ b = B ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
40 39 adantl
 |-  ( ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) /\ ( a = A /\ b = B ) ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = a /\ ( w ` N ) = b ) } = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
41 simprl
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> A e. V )
42 simprr
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> B e. V )
43 ovex
 |-  ( N WWalksN G ) e. _V
44 43 rabex
 |-  { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } e. _V
45 44 a1i
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } e. _V )
46 35 40 41 42 45 ovmpod
 |-  ( ( ( N e. NN0 /\ G e. _V ) /\ ( A e. V /\ B e. V ) ) -> ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) } )
47 11 34 46 ecase
 |-  ( A ( N WWalksNOn G ) B ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = A /\ ( w ` N ) = B ) }