Metamath Proof Explorer

Theorem pthhashvtx

Description: A graph containing a path has at least as many vertices as there are edges in the path. (Contributed by BTernaryTau, 5-Oct-2023)

Ref Expression
Hypothesis pthhashvtx.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion pthhashvtx ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 pthhashvtx.1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 hashfz0 ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) )
3 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
5 3 4 syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
6 nn0cn ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℂ )
7 npcan1 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℂ → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
8 5 6 7 3syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) = ( ♯ ‘ 𝐹 ) )
9 2 8 sylan9eqr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( ♯ ‘ 𝐹 ) )
10 1 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
11 3 10 syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 )
12 11 ffnd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
13 fzfi ⊢ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ Fin
14 resfnfinfin ⊢ ( ( 𝑃 Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) ∧ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ∈ Fin ) → ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Fin )
15 12 13 14 sylancl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Fin )
16 simpr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 )
17 fzssp1 ⊢ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) )
18 8 oveq2d ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 0 ... ( ( ( ♯ ‘ 𝐹 ) − 1 ) + 1 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
19 17 18 sseqtrid ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
20 11 19 fssresd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑉 )
21 20 adantr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑉 )
22 fz1ssfz0 ⊢ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) )
23 22 a1i ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
24 20 23 fssresd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑉 )
25 ispth ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
26 25 simp2bi ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
27 nn0z ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( ♯ ‘ 𝐹 ) ∈ ℤ )
28 fzoval ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℤ → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
29 27 28 syl ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
30 5 29 syl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) = ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
31 30 reseq2d ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
32 resabs1 ⊢ ( ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑃 ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
33 22 32 ax-mp ⊢ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑃 ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
34 31 33 eqtr4di ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
35 34 cnveqd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
36 35 funeqd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( Fun ◡ ( 𝑃 ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ Fun ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
37 26 36 mpbid ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → Fun ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
38 df-f1 ⊢ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 ↔ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⟶ 𝑉 ∧ Fun ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) )
39 24 37 38 sylanbrc ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 )
40 39 adantr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 )
41 38 simprbi ⊢ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 → Fun ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
42 40 41 syl ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → Fun ◡ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ↾ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
43 snsspr1 ⊢ { 0 } ⊆ { 0 , ( ♯ ‘ 𝐹 ) }
44 imass2 ⊢ ( { 0 } ⊆ { 0 , ( ♯ ‘ 𝐹 ) } → ( 𝑃 “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) )
45 43 44 ax-mp ⊢ ( 𝑃 “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } )
46 0elfz ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
47 46 snssd ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → { 0 } ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
48 resima2 ⊢ ( { 0 } ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) = ( 𝑃 “ { 0 } ) )
49 sseq1 ⊢ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) = ( 𝑃 “ { 0 } ) → ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ↔ ( 𝑃 “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ) )
50 47 48 49 3syl ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ↔ ( 𝑃 “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ) )
51 45 50 mpbiri ⊢ ( ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) )
52 resima2 ⊢ ( ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ⊆ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑃 “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
53 22 52 ax-mp ⊢ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑃 “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) )
54 30 imaeq2d ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) = ( 𝑃 “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) )
55 53 54 eqtr4id ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) = ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
56 55 ineq2d ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
57 25 simp3bi ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( 𝑃 “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
58 56 57 eqtrd ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ∅ )
59 ssdisj ⊢ ( ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ⊆ ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∧ ( ( 𝑃 “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ∅ ) → ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ∩ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ∅ )
60 51 58 59 syl2anr ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ { 0 } ) ∩ ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) “ ( 1 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ) = ∅ )
61 16 21 42 60 f1resfz0f1d ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 )
62 1 fvexi ⊢ 𝑉 ∈ V
63 hashf1dmcdm ⊢ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Fin ∧ 𝑉 ∈ V ∧ ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 ) → ( ♯ ‘ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ≤ ( ♯ ‘ 𝑉 ) )
64 62 63 mp3an2 ⊢ ( ( ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ∈ Fin ∧ ( 𝑃 ↾ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) : ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) –1-1→ 𝑉 ) → ( ♯ ‘ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ≤ ( ♯ ‘ 𝑉 ) )
65 15 61 64 syl2an2r ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ ( 0 ... ( ( ♯ ‘ 𝐹 ) − 1 ) ) ) ≤ ( ♯ ‘ 𝑉 ) )
66 9 65 eqbrtrrd ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
67 0nn0m1nnn0 ⊢ ( ( ♯ ‘ 𝐹 ) = 0 ↔ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ¬ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) )
68 67 biimpri ⊢ ( ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ∧ ¬ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) = 0 )
69 5 68 sylan ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ¬ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) = 0 )
70 hashge0 ⊢ ( 𝑉 ∈ V → 0 ≤ ( ♯ ‘ 𝑉 ) )
71 62 70 ax-mp ⊢ 0 ≤ ( ♯ ‘ 𝑉 )
72 69 71 eqbrtrdi ⊢ ( ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 ∧ ¬ ( ( ♯ ‘ 𝐹 ) − 1 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )
73 66 72 pm2.61dan ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ≤ ( ♯ ‘ 𝑉 ) )