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

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 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) }