Metamath Proof Explorer


Theorem pthsfval

Description: The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion pthsfval ( Paths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) }

Proof

Step Hyp Ref Expression
1 biidd ( 𝑔 = 𝐺 → ( ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ↔ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) )
2 df-pths Paths = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) } )
3 3anass ( ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ↔ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) )
4 3 opabbii { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) }
5 4 mpteq2i ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) } ) = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) } )
6 2 5 eqtri Paths = ( 𝑔 ∈ V ↦ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝑔 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) } )
7 1 6 fvmptopab ( Paths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) }
8 3anass ( ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ↔ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) )
9 8 opabbii { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) }
10 7 9 eqtr4i ( Paths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) }