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

Metamath Proof Explorer

Theorem 0spth

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

Ref Expression
Hypothesis 0pth.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0spth ( 𝐺 ∈ 𝑊 → ( ∅ ( SPaths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 0pth.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 0trl ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
3 2 anbi1d ⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ Fun ◡ 𝑃 ) ) )
4 isspth ⊢ ( ∅ ( SPaths ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ 𝑃 ) )
5 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
6 5 feq2i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ 𝑃 : { 0 } ⟶ 𝑉 )
7 c0ex ⊢ 0 ∈ V
8 7 fsn2 ⊢ ( 𝑃 : { 0 } ⟶ 𝑉 ↔ ( ( 𝑃 ‘ 0 ) ∈ 𝑉 ∧ 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } ) )
9 funcnvsn ⊢ Fun ◡ { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ }
10 cnveq ⊢ ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } → ◡ 𝑃 = ◡ { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } )
11 10 funeqd ⊢ ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } → ( Fun ◡ 𝑃 ↔ Fun ◡ { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } ) )
12 9 11 mpbiri ⊢ ( 𝑃 = { ⟨ 0 , ( 𝑃 ‘ 0 ) ⟩ } → Fun ◡ 𝑃 )
13 8 12 simplbiim ⊢ ( 𝑃 : { 0 } ⟶ 𝑉 → Fun ◡ 𝑃 )
14 6 13 sylbi ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → Fun ◡ 𝑃 )
15 14 pm4.71i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ↔ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ Fun ◡ 𝑃 ) )
16 3 4 15 3bitr4g ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( SPaths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )