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

Metamath Proof Explorer

Theorem wspthsn

Description: The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 11-May-2021)

Ref Expression
Assertion wspthsn ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 }

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( 𝑛 WWalksN 𝑔 ) = ( 𝑁 WWalksN 𝐺 ) )
2 fveq2 ⊢ ( 𝑔 = 𝐺 → ( SPaths ‘ 𝑔 ) = ( SPaths ‘ 𝐺 ) )
3 2 breqd ⊢ ( 𝑔 = 𝐺 → ( 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 ↔ 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
4 3 exbidv ⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
5 4 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → ( ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 ↔ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 ) )
6 1 5 rabeqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑔 = 𝐺 ) → { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } )
7 df-wspthsn ⊢ WSPathsN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( 𝑛 WWalksN 𝑔 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝑔 ) 𝑤 } )
8 ovex ⊢ ( 𝑁 WWalksN 𝐺 ) ∈ V
9 8 rabex ⊢ { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } ∈ V
10 6 7 9 ovmpoa ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } )
11 7 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WSPathsN 𝐺 ) = ∅ )
12 df-wwlksn ⊢ WWalksN = ( 𝑛 ∈ ℕ0 , 𝑔 ∈ V ↦ { 𝑤 ∈ ( WWalks ‘ 𝑔 ) ∣ ( ♯ ‘ 𝑤 ) = ( 𝑛 + 1 ) } )
13 12 mpondm0 ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WWalksN 𝐺 ) = ∅ )
14 13 rabeqdv ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = { 𝑤 ∈ ∅ ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } )
15 rab0 ⊢ { 𝑤 ∈ ∅ ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅
16 14 15 eqtrdi ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } = ∅ )
17 11 16 eqtr4d ⊢ ( ¬ ( 𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V ) → ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 } )
18 10 17 pm2.61i ⊢ ( 𝑁 WSPathsN 𝐺 ) = { 𝑤 ∈ ( 𝑁 WWalksN 𝐺 ) ∣ ∃ 𝑓 𝑓 ( SPaths ‘ 𝐺 ) 𝑤 }