Metamath Proof Explorer

Theorem uspgrlimlem4

Description: Lemma 4 for uspgrlim . (Contributed by AV, 16-Aug-2025)

Ref Expression
Hypotheses uspgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
uspgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
uspgrlim.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
uspgrlim.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
uspgrlim.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
uspgrlim.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
uspgrlim.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
uspgrlim.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion uspgrlimlem4 ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 uspgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 uspgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 uspgrlim.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑣 )
4 uspgrlim.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
5 uspgrlim.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
6 uspgrlim.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
7 uspgrlim.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
8 uspgrlim.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
9 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
10 9 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
11 f1of ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) )
12 10 11 syl ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) )
13 12 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) )
14 simpl ⊢ ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) )
15 fvco3 ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
16 15 fveq2d ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
17 13 14 16 syl2an ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
18 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
19 18 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
20 19 ad3antlr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
21 ssrab2 ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } ⊆ 𝐽
22 6 eqcomi ⊢ ( Edg ‘ 𝐻 ) = 𝐽
23 21 8 22 3sstr4i ⊢ 𝐿 ⊆ ( Edg ‘ 𝐻 )
24 f1of ⊢ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → 𝑔 : 𝐾 ⟶ 𝐿 )
25 24 adantr ⊢ ( ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐾 ⟶ 𝐿 )
26 25 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑔 : 𝐾 ⟶ 𝐿 )
27 26 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → 𝑔 : 𝐾 ⟶ 𝐿 )
28 13 ffund ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → Fun ( iEdg ‘ 𝐺 ) )
29 9 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
30 28 14 29 syl2an ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ ( Edg ‘ 𝐺 ) )
31 30 5 eleqtrrdi ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐼 )
32 simprr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 )
33 sseq1 ⊢ ( 𝑥 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( 𝑥 ⊆ 𝑁 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
34 33 7 elrab2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐼 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
35 31 32 34 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 )
36 27 35 ffvelcdmd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∈ 𝐿 )
37 23 36 sselid ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) )
38 f1ocnvfv2 ⊢ ( ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
39 20 37 38 syl2anc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
40 fvco3 ⊢ ( ( 𝑔 : 𝐾 ⟶ 𝐿 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
41 40 fveq2d ⊢ ( ( 𝑔 : 𝐾 ⟶ 𝐿 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
42 27 35 41 syl2anc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
43 5 eqcomi ⊢ ( Edg ‘ 𝐺 ) = 𝐼
44 feq3 ⊢ ( ( Edg ‘ 𝐺 ) = 𝐼 → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝐼 ) )
45 43 44 ax-mp ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝐼 )
46 45 biimpi ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( Edg ‘ 𝐺 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝐼 )
47 10 11 46 3syl ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝐼 )
48 47 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝐼 )
49 14 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) )
50 48 49 ffvelcdmd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐼 )
51 simprr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 )
52 50 51 34 sylanbrc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 )
53 imaeq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( 𝑓 “ 𝑒 ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
54 fveq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( 𝑔 ‘ 𝑒 ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
55 53 54 eqeq12d ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
56 55 rspcv ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐾 → ( ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
57 52 56 syl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
58 57 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
59 58 com23 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
60 59 adantld ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
61 60 imp31 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
62 39 42 61 3eqtr4d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
63 17 62 eqtr2d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) )
64 63 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )