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 ) ⟶ 𝑉 ) )