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

Metamath Proof Explorer

Theorem ispth

Description: Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Revised by AV, 29-Oct-2021)

Ref Expression
Assertion ispth ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 pthsfval ⊢ ( Paths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) }
2 3anass ⊢ ( ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ↔ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) )
3 2 opabbii ⊢ { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) } = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) }
4 1 3 eqtri ⊢ ( Paths ‘ 𝐺 ) = { ⟨ 𝑓 , 𝑝 ⟩ ∣ ( 𝑓 ( Trails ‘ 𝐺 ) 𝑝 ∧ ( Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ) }
5 simpr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → 𝑝 = 𝑃 )
6 fveq2 ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ 𝑓 ) = ( ♯ ‘ 𝐹 ) )
7 6 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
8 7 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 1 ..^ ( ♯ ‘ 𝑓 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
9 5 8 reseq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) = ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
10 9 cnveqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) = ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
11 10 funeqd ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ↔ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
12 6 preq2d ⊢ ( 𝑓 = 𝐹 → { 0 , ( ♯ ‘ 𝑓 ) } = { 0 , ( ♯ ‘ 𝐹 ) } )
13 12 adantr ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → { 0 , ( ♯ ‘ 𝑓 ) } = { 0 , ( ♯ ‘ 𝐹 ) } )
14 5 13 imaeq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) = ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) )
15 5 8 imaeq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) = ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
16 14 15 ineq12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
17 16 eqeq1d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ↔ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
18 11 17 anbi12d ⊢ ( ( 𝑓 = 𝐹 ∧ 𝑝 = 𝑃 ) → ( ( Fun ◡ ( 𝑝 ↾ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ∧ ( ( 𝑝 “ { 0 , ( ♯ ‘ 𝑓 ) } ) ∩ ( 𝑝 “ ( 1 ..^ ( ♯ ‘ 𝑓 ) ) ) ) = ∅ ) ↔ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) )
19 reltrls ⊢ Rel ( Trails ‘ 𝐺 )
20 4 18 19 brfvopabrbr ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) )
21 3anass ⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) )
22 20 21 bitr4i ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )