Theorem spthispth

Description: A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017) (Revised by AV, 9-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Assertion	spthispth	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
2		funres11	⊢ ( Fun ◡ 𝑃 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
3	2	adantl	⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
4		imain	⊢ ( Fun ◡ 𝑃 → ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
5		1e0p1	⊢ 1 = ( 0 + 1 )
6	5	oveq1i	⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) )
7	6	ineq2i	⊢ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) )
8		0z	⊢ 0 ∈ ℤ
9		prinfzo0	⊢ ( 0 ∈ ℤ → ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅ )
10	8 9	ax-mp	⊢ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( ( 0 + 1 ) ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
11	7 10	eqtri	⊢ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ∅
12	11	imaeq2i	⊢ ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( 𝑃 “ ∅ )
13		ima0	⊢ ( 𝑃 “ ∅ ) = ∅
14	12 13	eqtri	⊢ ( 𝑃 “ ( { 0 , ( ♯ ‘ 𝐹 ) } ∩ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅
15	4 14	eqtr3di	⊢ ( Fun ◡ 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
16	15	adantl	⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
17	1 3 16	3jca	⊢ ( ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
18		isspth	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
19		ispth	⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
20	17 18 19	3imtr4i	⊢ ( 𝐹 ( SPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )