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