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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion iswwlksnon ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) }

Proof

Step Hyp Ref Expression
1 iswwlksnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 0ov ⊢ ( 𝐴 ∅ 𝐵 ) = ∅
3 df-wwlksnon ⊢ WWalksNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑛 ) = 𝑏 ) } ) )
4 3 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksNOn 𝐺 ) = ∅ )
5 4 oveqd ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ( 𝐴 ∅ 𝐵 ) )
6 df-wwlksn ⊢ WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )
7 6 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )
8 7 rabeqdv ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } = { 𝑤 ∈ ∅ ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
9 rab0 ⊢ { 𝑤 ∈ ∅ ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } = ∅
10 8 9 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } = ∅ )
11 2 5 10 3eqtr4a ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
12 1 wwlksnon ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
13 12 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
14 13 oveqd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) 𝐵 ) )
15 eqid ⊢ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } )
16 15 mpondm0 ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) 𝐵 ) = ∅ )
17 16 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) 𝐵 ) = ∅ )
18 14 17 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )
19 18 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ ) )
20 5 2 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )
21 20 a1d ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ ) )
22 19 21 pm2.61i ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )
23 1 wwlknllvtx ⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( 𝑤 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑤 ‘ 𝑁 ) ∈ 𝑉 ) )
24 eleq1 ⊢ ( 𝐴 = ( 𝑤 ‘ 0 ) → ( 𝐴 ∈ 𝑉 ↔ ( 𝑤 ‘ 0 ) ∈ 𝑉 ) )
25 24 eqcoms ⊢ ( ( 𝑤 ‘ 0 ) = 𝐴 → ( 𝐴 ∈ 𝑉 ↔ ( 𝑤 ‘ 0 ) ∈ 𝑉 ) )
26 eleq1 ⊢ ( 𝐵 = ( 𝑤 ‘ 𝑁 ) → ( 𝐵 ∈ 𝑉 ↔ ( 𝑤 ‘ 𝑁 ) ∈ 𝑉 ) )
27 26 eqcoms ⊢ ( ( 𝑤 ‘ 𝑁 ) = 𝐵 → ( 𝐵 ∈ 𝑉 ↔ ( 𝑤 ‘ 𝑁 ) ∈ 𝑉 ) )
28 25 27 bi2anan9 ⊢ ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ↔ ( ( 𝑤 ‘ 0 ) ∈ 𝑉 ∧ ( 𝑤 ‘ 𝑁 ) ∈ 𝑉 ) ) )
29 23 28 syl5ibrcom ⊢ ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ( ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
30 29 con3rr3 ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) → ¬ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) ) )
31 30 ralrimiv ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) )
32 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } = ∅ ↔ ∀ 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ¬ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) )
33 31 32 sylibr ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } = ∅ )
34 22 33 eqtr4d ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
35 12 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑁 WWalksNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } ) )
36 eqeq2 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑤 ‘ 0 ) = 𝑎 ↔ ( 𝑤 ‘ 0 ) = 𝐴 ) )
37 eqeq2 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑤 ‘ 𝑁 ) = 𝑏 ↔ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) )
38 36 37 bi2anan9 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) ↔ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) ) )
39 38 rabbidv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
40 39 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝑎 ∧ ( 𝑤 ‘ 𝑁 ) = 𝑏 ) } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
41 simprl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
42 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
43 ovex ⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V
44 43 rabex ⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } ∈ V
45 44 a1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } ∈ V )
46 35 40 41 42 45 ovmpod ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) } )
47 11 34 46 ecase ⊢ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ( ( 𝑤 ‘ 0 ) = 𝐴 ∧ ( 𝑤 ‘ 𝑁 ) = 𝐵 ) }