Theorem trlontrl

Description: A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021)

	Ref	Expression
Assertion	trlontrl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		trliswlk	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
2		wlkonwlk	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )
3	1 2	syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )
4		id	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
5		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6	5	wlkepvtx	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) )
7		wlkv	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
8		3simpc	⊢ ( ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) → ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) )
9	8	anim2i	⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
10	6 7 9	syl2anc	⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
11	1 10	syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) )
12	5	istrlson	⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ ( Vtx ‘ 𝐺 ) ∧ ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝐹 ∈ V ∧ 𝑃 ∈ V ) ) → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
13	11 12	syl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ↔ ( 𝐹 ( ( 𝑃 ‘ 0 ) ( WalksOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) ) )
14	3 4 13	mpbir2and	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → 𝐹 ( ( 𝑃 ‘ 0 ) ( TrailsOn ‘ 𝐺 ) ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) 𝑃 )