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