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 ) }