Metamath Proof Explorer

Theorem upgrimspths

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

Ref Expression
Hypotheses upgrimwlk.i ⊢ I = iEdg ⁡ G
upgrimwlk.j ⊢ J = iEdg ⁡ H
upgrimwlk.g ⊢ φ → G ∈ USHGraph
upgrimwlk.h ⊢ φ → H ∈ USHGraph
upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
upgrimspths.s ⊢ φ → F SPaths ⁡ G P
Assertion upgrimspths ⊢ φ → E SPaths ⁡ H N ∘ P

Proof

Step Hyp Ref Expression
1 upgrimwlk.i ⊢ I = iEdg ⁡ G
2 upgrimwlk.j ⊢ J = iEdg ⁡ H
3 upgrimwlk.g ⊢ φ → G ∈ USHGraph
4 upgrimwlk.h ⊢ φ → H ∈ USHGraph
5 upgrimwlk.n ⊢ φ → N ∈ G GraphIso H
6 upgrimwlk.e ⊢ E = x ∈ dom ⁡ F ⟼ J -1 ⁡ N I ⁡ F ⁡ x
7 upgrimspths.s ⊢ φ → F SPaths ⁡ G P
8 spthispth ⊢ F SPaths ⁡ G P → F Paths ⁡ G P
9 pthistrl ⊢ F Paths ⁡ G P → F Trails ⁡ G P
10 7 8 9 3syl ⊢ φ → F Trails ⁡ G P
11 1 2 3 4 5 6 10 upgrimtrls ⊢ φ → E Trails ⁡ H N ∘ P
12 isspth ⊢ F SPaths ⁡ G P ↔ F Trails ⁡ G P ∧ Fun ⁡ P -1
13 12 simprbi ⊢ F SPaths ⁡ G P → Fun ⁡ P -1
14 7 13 syl ⊢ φ → Fun ⁡ P -1
15 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
16 eqid ⊢ Vtx ⁡ H = Vtx ⁡ H
17 15 16 grimf1o ⊢ N ∈ G GraphIso H → N : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
18 dff1o3 ⊢ N : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ↔ N : Vtx ⁡ G ⟶ onto Vtx ⁡ H ∧ Fun ⁡ N -1
19 18 simprbi ⊢ N : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → Fun ⁡ N -1
20 5 17 19 3syl ⊢ φ → Fun ⁡ N -1
21 funco ⊢ Fun ⁡ P -1 ∧ Fun ⁡ N -1 → Fun ⁡ P -1 ∘ N -1
22 14 20 21 syl2anc ⊢ φ → Fun ⁡ P -1 ∘ N -1
23 cnvco ⊢ N ∘ P -1 = P -1 ∘ N -1
24 23 funeqi ⊢ Fun ⁡ N ∘ P -1 ↔ Fun ⁡ P -1 ∘ N -1
25 22 24 sylibr ⊢ φ → Fun ⁡ N ∘ P -1
26 isspth ⊢ E SPaths ⁡ H N ∘ P ↔ E Trails ⁡ H N ∘ P ∧ Fun ⁡ N ∘ P -1
27 11 25 26 sylanbrc ⊢ φ → E SPaths ⁡ H N ∘ P