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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion iswspthsnon ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 }

Proof

Step Hyp Ref Expression
1 iswspthsnon.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 0ov ⊢ ( 𝐴 ∅ 𝐵 ) = ∅
3 df-wspthsnon ⊢ WSPathsNOn = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ ( 𝑎 ∈ ( Vtx ‘ 𝑔 ) , 𝑏 ∈ ( Vtx ‘ 𝑔 ) ↦ { 𝑤 ∈ ( 𝑎 ( 𝑛 WWalksNOn 𝑔 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝑔 ) 𝑏 ) 𝑤 } ) )
4 3 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WSPathsNOn 𝐺 ) = ∅ )
5 4 oveqd ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ∅ 𝐵 ) )
6 id ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) )
7 6 intnanrd ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ¬ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) )
8 1 wwlksnon0 ⊢ ( ¬ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )
9 7 8 syl ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) = ∅ )
10 9 rabeqdv ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = { 𝑤 ∈ ∅ ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
11 rab0 ⊢ { 𝑤 ∈ ∅ ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = ∅
12 10 11 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = ∅ )
13 2 5 12 3eqtr4a ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
14 1 wspthsnon ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WSPathsNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) )
15 14 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑁 WSPathsNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) )
16 15 oveqd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) 𝐵 ) )
17 eqid ⊢ ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } )
18 17 mpondm0 ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) 𝐵 ) = ∅ )
19 18 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) 𝐵 ) = ∅ )
20 16 19 eqtrd ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ∅ )
21 20 ex ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ∅ ) )
22 5 2 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ∅ )
23 22 a1d ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ∅ ) )
24 21 23 pm2.61i ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = ∅ )
25 1 wwlksonvtx ⊢ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
26 25 pm2.24d ⊢ ( 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) → ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ¬ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
27 26 impcom ⊢ ( ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ) → ¬ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
28 27 nexdv ⊢ ( ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ) → ¬ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
29 28 ralrimiva ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ∀ 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ¬ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
30 rabeq0 ⊢ ( { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = ∅ ↔ ∀ 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ¬ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 )
31 29 30 sylibr ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } = ∅ )
32 24 31 eqtr4d ⊢ ( ¬ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
33 14 adantr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑁 WSPathsNOn 𝐺 ) = ( 𝑎 ∈ 𝑉 , 𝑏 ∈ 𝑉 ↦ { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } ) )
34 oveq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) = ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) )
35 oveq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) = ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) )
36 35 breqd ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 ↔ 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
37 36 exbidv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 ) )
38 34 37 rabeqbidv ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
39 38 adantl ⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → { 𝑤 ∈ ( 𝑎 ( 𝑁 WWalksNOn 𝐺 ) 𝑏 ) ∣ ∃ 𝑓 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑤 } = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
40 simprl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
41 simprr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
42 ovex ⊢ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∈ V
43 42 rabex ⊢ { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } ∈ V
44 43 a1i ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } ∈ V )
45 33 39 40 41 44 ovmpod ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 } )
46 13 32 45 ecase ⊢ ( 𝐴 ( 𝑁 WSPathsNOn 𝐺 ) 𝐵 ) = { 𝑤 ∈ ( 𝐴 ( 𝑁 WWalksNOn 𝐺 ) 𝐵 ) ∣ ∃ 𝑓 𝑓 ( 𝐴 ( SPathsOn ‘ 𝐺 ) 𝐵 ) 𝑤 }