Metamath Proof Explorer

Theorem upgrimtrlslem1

Description: Lemma 1 for upgrimtrls . (Contributed by AV, 29-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
upgrimtrls.t ⊢ φ → F Trails ⁡ G P
Assertion upgrimtrlslem1 ⊢ φ ∧ X ∈ dom ⁡ F → N I ⁡ F ⁡ X ∈ Edg ⁡ H

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 upgrimtrls.t ⊢ φ → F Trails ⁡ G P
8 uspgruhgr ⊢ G ∈ USHGraph → G ∈ UHGraph
9 3 8 syl ⊢ φ → G ∈ UHGraph
10 uspgruhgr ⊢ H ∈ USHGraph → H ∈ UHGraph
11 4 10 syl ⊢ φ → H ∈ UHGraph
12 9 11 jca ⊢ φ → G ∈ UHGraph ∧ H ∈ UHGraph
13 12 adantr ⊢ φ ∧ X ∈ dom ⁡ F → G ∈ UHGraph ∧ H ∈ UHGraph
14 5 adantr ⊢ φ ∧ X ∈ dom ⁡ F → N ∈ G GraphIso H
15 1 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ I
16 9 15 syl ⊢ φ → Fun ⁡ I
17 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
18 1 wlkf ⊢ F Walks ⁡ G P → F ∈ Word dom ⁡ I
19 wrdf ⊢ F ∈ Word dom ⁡ I → F : 0 ..^ F ⟶ dom ⁡ I
20 19 ffdmd ⊢ F ∈ Word dom ⁡ I → F : dom ⁡ F ⟶ dom ⁡ I
21 18 20 syl ⊢ F Walks ⁡ G P → F : dom ⁡ F ⟶ dom ⁡ I
22 7 17 21 3syl ⊢ φ → F : dom ⁡ F ⟶ dom ⁡ I
23 22 ffvelcdmda ⊢ φ ∧ X ∈ dom ⁡ F → F ⁡ X ∈ dom ⁡ I
24 1 iedgedg ⊢ Fun ⁡ I ∧ F ⁡ X ∈ dom ⁡ I → I ⁡ F ⁡ X ∈ Edg ⁡ G
25 16 23 24 syl2an2r ⊢ φ ∧ X ∈ dom ⁡ F → I ⁡ F ⁡ X ∈ Edg ⁡ G
26 eqid ⊢ Edg ⁡ G = Edg ⁡ G
27 eqid ⊢ Edg ⁡ H = Edg ⁡ H
28 26 27 uhgrimedgi ⊢ G ∈ UHGraph ∧ H ∈ UHGraph ∧ N ∈ G GraphIso H ∧ I ⁡ F ⁡ X ∈ Edg ⁡ G → N I ⁡ F ⁡ X ∈ Edg ⁡ H
29 13 14 25 28 syl12anc ⊢ φ ∧ X ∈ dom ⁡ F → N I ⁡ F ⁡ X ∈ Edg ⁡ H