Metamath Proof Explorer

Theorem uspgrlimlem3

Description: Lemma 3 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 uspgrlimlem3 ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –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 sseq1 ⊢ ( 𝑥 = 𝑒 → ( 𝑥 ⊆ 𝑁 ↔ 𝑒 ⊆ 𝑁 ) )
10 9 7 elrab2 ⊢ ( 𝑒 ∈ 𝐾 ↔ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) )
11 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
12 11 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
13 f1ocnv ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) → ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐺 ) )
14 f1of ⊢ ( ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐺 ) → ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐺 ) )
15 12 13 14 3syl ⊢ ( 𝐺 ∈ USPGraph → ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐺 ) )
16 15 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐺 ) )
17 5 eleq2i ⊢ ( 𝑒 ∈ 𝐼 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
18 17 biimpi ⊢ ( 𝑒 ∈ 𝐼 → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
19 18 adantr ⊢ ( ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
20 fvco3 ⊢ ( ( ◡ ( iEdg ‘ 𝐺 ) : ( Edg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐺 ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) )
21 16 19 20 syl2an ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) )
22 f1ocnvdm ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ dom ( iEdg ‘ 𝐺 ) )
23 12 19 22 syl2an ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ dom ( iEdg ‘ 𝐺 ) )
24 f1ocnvfv2 ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = 𝑒 )
25 12 19 24 syl2an ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = 𝑒 )
26 simprr ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → 𝑒 ⊆ 𝑁 )
27 25 26 eqsstrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ⊆ 𝑁 )
28 23 27 jca ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ⊆ 𝑁 ) )
29 28 adantlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ⊆ 𝑁 ) )
30 fveq2 ⊢ ( 𝑥 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) )
31 30 sseq1d ⊢ ( 𝑥 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ⊆ 𝑁 ) )
32 31 elrab ⊢ ( ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ↔ ( ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ⊆ 𝑁 ) )
33 29 32 sylibr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } )
34 fveq2 ⊢ ( 𝑖 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) )
35 34 imaeq2d ⊢ ( 𝑖 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) )
36 2fveq3 ⊢ ( 𝑖 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) )
37 35 36 eqeq12d ⊢ ( 𝑖 = ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) )
38 37 rspcv ⊢ ( ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) )
39 33 38 syl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) )
40 eqcom ⊢ ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) )
41 f1of ⊢ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 → ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⟶ 𝑅 )
42 41 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⟶ 𝑅 )
43 42 33 fvco3d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) )
44 43 eqcomd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) )
45 12 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
46 45 19 24 syl2an ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = 𝑒 )
47 46 imaeq2d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( 𝑓 “ 𝑒 ) )
48 44 47 eqeq12d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ↔ ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) )
49 48 biimpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) )
50 40 49 biimtrid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) )
51 39 50 syld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) )
52 51 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) → ( ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) ) )
53 52 com23 ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) ) )
54 53 ex ⊢ ( 𝐺 ∈ USPGraph → ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) → ( ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) ) ) ) )
55 54 3imp1 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ‘ ( ◡ ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) = ( 𝑓 “ 𝑒 ) )
56 21 55 eqtr2d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ∧ ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) ) → ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) )
57 56 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ( ( 𝑒 ∈ 𝐼 ∧ 𝑒 ⊆ 𝑁 ) → ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
58 10 57 biimtrid ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ 𝑅 ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑒 ∈ 𝐾 → ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )