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

Metamath Proof Explorer

Theorem 0trl

Description: A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 7-Jan-2021) (Revised by AV, 30-Oct-2021)

Ref Expression
Hypothesis 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0trl ( 𝐺 ∈ 𝑈 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 0wlk ⊢ ( 𝐺 ∈ 𝑈 → ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
3 2 anbi1d ⊢ ( 𝐺 ∈ 𝑈 → ( ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ∅ ) ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ Fun ◡ ∅ ) ) )
4 istrl ⊢ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ∅ ) )
5 funcnv0 ⊢ Fun ◡ ∅
6 5 biantru ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ Fun ◡ ∅ ) )
7 3 4 6 3bitr4g ⊢ ( 𝐺 ∈ 𝑈 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )