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 ‘ 𝐺 ) 𝑤 }