Metamath Proof Explorer

Theorem upgrimpths

Description: Graph isomorphisms between simple pseudographs map paths onto paths. (Contributed by AV, 31-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
upgrimpths.p ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
Assertion upgrimpths ( 𝜑 → 𝐸 ( Paths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 upgrimwlk.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
3 upgrimwlk.g ⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
4 upgrimwlk.h ⊢ ( 𝜑 → 𝐻 ∈ USPGraph )
5 upgrimwlk.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝐺 GraphIso 𝐻 ) )
6 upgrimwlk.e ⊢ 𝐸 = ( 𝑥 ∈ dom 𝐹 ↦ ( ◡ 𝐽 ‘ ( 𝑁 “ ( 𝐼 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
7 upgrimpths.p ⊢ ( 𝜑 → 𝐹 ( Paths ‘ 𝐺 ) 𝑃 )
8 pthistrl ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
9 7 8 syl ⊢ ( 𝜑 → 𝐹 ( Trails ‘ 𝐺 ) 𝑃 )
10 1 2 3 4 5 6 9 upgrimtrls ⊢ ( 𝜑 → 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )
11 1 2 3 4 5 6 7 upgrimpthslem1 ⊢ ( 𝜑 → Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
12 pthiswlk ⊢ ( 𝐹 ( Paths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
13 1 wlkf ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝐹 ∈ Word dom 𝐼 )
14 7 12 13 3syl ⊢ ( 𝜑 → 𝐹 ∈ Word dom 𝐼 )
15 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
16 15 wlkp ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
17 7 12 16 3syl ⊢ ( 𝜑 → 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) )
18 1 2 3 4 5 6 14 17 upgrimwlklem4 ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) )
19 18 ffnd ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) Fn ( 0 ... ( ♯ ‘ 𝐸 ) ) )
20 1 2 3 4 5 6 14 upgrimwlklem1 ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) )
21 wlkcl ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
22 7 12 21 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ℕ0 )
23 20 22 eqeltrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐸 ) ∈ ℕ0 )
24 0elfz ⊢ ( ( ♯ ‘ 𝐸 ) ∈ ℕ0 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐸 ) ) )
25 23 24 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... ( ♯ ‘ 𝐸 ) ) )
26 nn0fz0 ⊢ ( ( ♯ ‘ 𝐹 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
27 22 26 sylib ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
28 20 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐸 ) ) = ( 0 ... ( ♯ ‘ 𝐹 ) ) )
29 27 28 eleqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐸 ) ) )
30 fnimapr ⊢ ( ( ( 𝑁 ∘ 𝑃 ) Fn ( 0 ... ( ♯ ‘ 𝐸 ) ) ∧ 0 ∈ ( 0 ... ( ♯ ‘ 𝐸 ) ) ∧ ( ♯ ‘ 𝐹 ) ∈ ( 0 ... ( ♯ ‘ 𝐸 ) ) ) → ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) } )
31 19 25 29 30 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) = { ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) } )
32 31 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ↔ 𝑥 ∈ { ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) } ) )
33 vex ⊢ 𝑥 ∈ V
34 33 elpr ⊢ ( 𝑥 ∈ { ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) , ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) } ↔ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
35 32 34 bitrdi ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ↔ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) )
36 1 2 3 4 5 6 7 upgrimpthslem2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∧ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
37 36 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) )
38 eqeq2 ⊢ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) → ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ↔ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ) )
39 38 notbid ⊢ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) → ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ↔ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ) )
40 37 39 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ) )
41 36 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) )
42 eqeq2 ⊢ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) → ( ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ↔ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
43 42 notbid ⊢ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) → ( ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ↔ ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) )
44 41 43 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ) )
45 40 44 jaod ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ( ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ) )
46 45 impancom ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ) )
47 46 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) ∧ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) → ¬ ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 )
48 47 nrexdv ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ¬ ∃ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 )
49 20 eqcomd ⊢ ( 𝜑 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ 𝐸 ) )
50 49 oveq2d ⊢ ( 𝜑 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... ( ♯ ‘ 𝐸 ) ) )
51 50 feq2d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐻 ) ↔ ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐸 ) ) ⟶ ( Vtx ‘ 𝐻 ) ) )
52 18 51 mpbird ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐻 ) )
53 52 ffnd ⊢ ( 𝜑 → ( 𝑁 ∘ 𝑃 ) Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
54 53 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑁 ∘ 𝑃 ) Fn ( 0 ... ( ♯ ‘ 𝐹 ) ) )
55 fzo0ss1 ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ..^ ( ♯ ‘ 𝐹 ) )
56 fzossfz ⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
57 55 56 sstri ⊢ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) )
58 57 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ⊆ ( 0 ... ( ♯ ‘ 𝐹 ) ) )
59 54 58 fvelimabd ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ( 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ↔ ∃ 𝑦 ∈ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ( ( 𝑁 ∘ 𝑃 ) ‘ 𝑦 ) = 𝑥 ) )
60 48 59 mtbird ⊢ ( ( 𝜑 ∧ ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) ) → ¬ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
61 60 ex ⊢ ( 𝜑 → ( ( 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ 0 ) ∨ 𝑥 = ( ( 𝑁 ∘ 𝑃 ) ‘ ( ♯ ‘ 𝐹 ) ) ) → ¬ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
62 35 61 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) → ¬ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
63 62 ralrimiv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ¬ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
64 disj ⊢ ( ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ↔ ∀ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ¬ 𝑥 ∈ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
65 63 64 sylibr ⊢ ( 𝜑 → ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ )
66 20 oveq2d ⊢ ( 𝜑 → ( 1 ..^ ( ♯ ‘ 𝐸 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
67 66 reseq2d ⊢ ( 𝜑 → ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) = ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
68 67 cnveqd ⊢ ( 𝜑 → ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) = ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
69 68 funeqd ⊢ ( 𝜑 → ( Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ↔ Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
70 preq2 ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → { 0 , ( ♯ ‘ 𝐸 ) } = { 0 , ( ♯ ‘ 𝐹 ) } )
71 70 imaeq2d ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) = ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) )
72 oveq2 ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → ( 1 ..^ ( ♯ ‘ 𝐸 ) ) = ( 1 ..^ ( ♯ ‘ 𝐹 ) ) )
73 72 imaeq2d ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) = ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) )
74 71 73 ineq12d ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
75 74 eqeq1d ⊢ ( ( ♯ ‘ 𝐸 ) = ( ♯ ‘ 𝐹 ) → ( ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ∅ ↔ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
76 20 75 syl ⊢ ( 𝜑 → ( ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ∅ ↔ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) )
77 69 76 3anbi23d ⊢ ( 𝜑 → ( ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ∅ ) ↔ ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ∧ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐹 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ∅ ) ) )
78 10 11 65 77 mpbir3and ⊢ ( 𝜑 → ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ∅ ) )
79 ispth ⊢ ( 𝐸 ( Paths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ↔ ( 𝐸 ( Trails ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) ∧ Fun ◡ ( ( 𝑁 ∘ 𝑃 ) ↾ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ∧ ( ( ( 𝑁 ∘ 𝑃 ) “ { 0 , ( ♯ ‘ 𝐸 ) } ) ∩ ( ( 𝑁 ∘ 𝑃 ) “ ( 1 ..^ ( ♯ ‘ 𝐸 ) ) ) ) = ∅ ) )
80 78 79 sylibr ⊢ ( 𝜑 → 𝐸 ( Paths ‘ 𝐻 ) ( 𝑁 ∘ 𝑃 ) )