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

Metamath Proof Explorer

Theorem 0pth

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

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

Proof

Step Hyp Ref Expression
1 0pth.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 ispth ⊢ ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) )
3 2 a1i ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) )
4 3anass ⊢ ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) )
5 4 a1i ⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) ) )
6 funcnv0 ⊢ Fun ◡ ∅
7 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
8 0le1 ⊢ 0 ≤ 1
9 7 8 eqbrtri ⊢ ( ♯ ‘ ∅ ) ≤ 1
10 1z ⊢ 1 ∈ ℤ
11 0z ⊢ 0 ∈ ℤ
12 7 11 eqeltri ⊢ ( ♯ ‘ ∅ ) ∈ ℤ
13 fzon ⊢ ( ( 1 ∈ ℤ ∧ ( ♯ ‘ ∅ ) ∈ ℤ ) → ( ( ♯ ‘ ∅ ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅ ) )
14 10 12 13 mp2an ⊢ ( ( ♯ ‘ ∅ ) ≤ 1 ↔ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅ )
15 9 14 mpbi ⊢ ( 1 ..^ ( ♯ ‘ ∅ ) ) = ∅
16 15 reseq2i ⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ( 𝑃 ↾ ∅ )
17 res0 ⊢ ( 𝑃 ↾ ∅ ) = ∅
18 16 17 eqtri ⊢ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ∅
19 18 cnveqi ⊢ ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ◡ ∅
20 19 funeqi ⊢ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ↔ Fun ◡ ∅ )
21 6 20 mpbir ⊢ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) )
22 15 imaeq2i ⊢ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ( 𝑃 “ ∅ )
23 ima0 ⊢ ( 𝑃 “ ∅ ) = ∅
24 22 23 eqtri ⊢ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) = ∅
25 24 ineq2i ⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ∅ )
26 in0 ⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ∅ ) = ∅
27 25 26 eqtri ⊢ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅
28 21 27 pm3.2i ⊢ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ )
29 28 biantru ⊢ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ) )
30 5 29 bitr4di ⊢ ( 𝐺 ∈ 𝑊 → ( ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ ∅ ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ ∅ ) ) ) ) = ∅ ) ↔ ∅ ( Trails ‘ 𝐺 ) 𝑃 ) )
31 1 0trl ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Trails ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )
32 3 30 31 3bitrd ⊢ ( 𝐺 ∈ 𝑊 → ( ∅ ( Paths ‘ 𝐺 ) 𝑃 ↔ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) )