Metamath Proof Explorer

Theorem uspgrlim

Description: A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 ). (Contributed by AV, 15-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 uspgrlim ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) ) )

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 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
11 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 }
12 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 }
13 1 2 3 4 9 10 11 12 isgrlim2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) ) )
14 fvex ⊢ ( iEdg ‘ 𝐻 ) ∈ V
15 vex ⊢ ℎ ∈ V
16 14 15 coex ⊢ ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∈ V
17 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
18 17 cnvex ⊢ ◡ ( iEdg ‘ 𝐺 ) ∈ V
19 16 18 coex ⊢ ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ∈ V
20 19 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ∈ V )
21 9 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
22 21 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
23 simprl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )
24 10 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
25 24 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
26 ssrab2 ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 )
27 ssrab2 ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 )
28 26 27 pm3.2i ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 ) )
29 28 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 ) ) )
30 3f1oss1 ⊢ ( ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ) ∧ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom ( iEdg ‘ 𝐻 ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) –1-1-onto→ ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
31 22 23 25 29 30 syl31anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) –1-1-onto→ ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
32 eqidd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) )
33 3 5 7 uspgrlimlem1 ⊢ ( 𝐺 ∈ USPGraph → 𝐾 = ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) )
34 33 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → 𝐾 = ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) )
35 4 6 8 uspgrlimlem1 ⊢ ( 𝐻 ∈ USPGraph → 𝐿 = ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
36 35 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → 𝐿 = ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
37 32 34 36 f1oeq123d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : 𝐾 –1-1-onto→ 𝐿 ↔ ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) –1-1-onto→ ( ( iEdg ‘ 𝐻 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) ) )
38 31 37 mpbird ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : 𝐾 –1-1-onto→ 𝐿 )
39 simpll ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → 𝐺 ∈ USPGraph )
40 simprr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) )
41 1 2 3 4 5 6 7 8 uspgrlimlem3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ( 𝑒 ∈ 𝐾 → ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
42 39 23 40 41 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( 𝑒 ∈ 𝐾 → ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
43 42 ralrimiv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) )
44 38 43 jca ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
45 f1oeq1 ⊢ ( 𝑔 = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ↔ ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : 𝐾 –1-1-onto→ 𝐿 ) )
46 fveq1 ⊢ ( 𝑔 = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) → ( 𝑔 ‘ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) )
47 46 eqeq2d ⊢ ( 𝑔 = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
48 47 ralbidv ⊢ ( 𝑔 = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) )
49 45 48 anbi12d ⊢ ( 𝑔 = ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) → ( ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( ( ( ( iEdg ‘ 𝐻 ) ∘ ℎ ) ∘ ◡ ( iEdg ‘ 𝐺 ) ) ‘ 𝑒 ) ) ) )
50 20 44 49 spcedv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) → ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) )
51 50 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
52 51 exlimdv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) → ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
53 14 cnvex ⊢ ◡ ( iEdg ‘ 𝐻 ) ∈ V
54 vex ⊢ 𝑔 ∈ V
55 53 54 coex ⊢ ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∈ V
56 55 17 coex ⊢ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ∈ V
57 56 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ∈ V )
58 21 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) )
59 simprl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
60 24 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) )
61 5 rabeqi ⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 } = { 𝑥 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑥 ⊆ 𝑁 }
62 7 61 eqtri ⊢ 𝐾 = { 𝑥 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑥 ⊆ 𝑁 }
63 62 ssrab3 ⊢ 𝐾 ⊆ ( Edg ‘ 𝐺 )
64 6 rabeqi ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 } = { 𝑥 ∈ ( Edg ‘ 𝐻 ) ∣ 𝑥 ⊆ 𝑀 }
65 8 64 eqtri ⊢ 𝐿 = { 𝑥 ∈ ( Edg ‘ 𝐻 ) ∣ 𝑥 ⊆ 𝑀 }
66 65 ssrab3 ⊢ 𝐿 ⊆ ( Edg ‘ 𝐻 )
67 63 66 pm3.2i ⊢ ( 𝐾 ⊆ ( Edg ‘ 𝐺 ) ∧ 𝐿 ⊆ ( Edg ‘ 𝐻 ) )
68 67 a1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝐾 ⊆ ( Edg ‘ 𝐺 ) ∧ 𝐿 ⊆ ( Edg ‘ 𝐻 ) ) )
69 3f1oss2 ⊢ ( ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) –1-1-onto→ ( Edg ‘ 𝐻 ) ) ∧ ( 𝐾 ⊆ ( Edg ‘ 𝐺 ) ∧ 𝐿 ⊆ ( Edg ‘ 𝐻 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : ( ◡ ( iEdg ‘ 𝐺 ) “ 𝐾 ) –1-1-onto→ ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) )
70 58 59 60 68 69 syl31anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : ( ◡ ( iEdg ‘ 𝐺 ) “ 𝐾 ) –1-1-onto→ ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) )
71 eqidd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) )
72 3 5 7 uspgrlimlem2 ⊢ ( 𝐺 ∈ USPGraph → ( ◡ ( iEdg ‘ 𝐺 ) “ 𝐾 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } )
73 72 ad2antrr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ◡ ( iEdg ‘ 𝐺 ) “ 𝐾 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } )
74 4 6 8 uspgrlimlem2 ⊢ ( 𝐻 ∈ USPGraph → ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )
75 74 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )
76 71 73 75 f1oeq123d ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : ( ◡ ( iEdg ‘ 𝐺 ) “ 𝐾 ) –1-1-onto→ ( ◡ ( iEdg ‘ 𝐻 ) “ 𝐿 ) ↔ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
77 70 76 mpbid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } )
78 fveq2 ⊢ ( 𝑥 = 𝑖 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
79 78 sseq1d ⊢ ( 𝑥 = 𝑖 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
80 79 elrab ⊢ ( 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ↔ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
81 1 2 3 4 5 6 7 8 uspgrlimlem4 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )
82 80 81 biimtrid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )
83 82 ralrimiv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) )
84 77 83 jca ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )
85 f1oeq1 ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ↔ ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ) )
86 fveq1 ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ℎ ‘ 𝑖 ) = ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) )
87 86 fveq2d ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) )
88 87 eqeq2d ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )
89 88 ralbidv ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) )
90 85 89 anbi12d ⊢ ( ℎ = ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) → ( ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( ( ◡ ( iEdg ‘ 𝐻 ) ∘ 𝑔 ) ∘ ( iEdg ‘ 𝐺 ) ) ‘ 𝑖 ) ) ) ) )
91 57 84 90 spcedv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) )
92 91 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
93 92 exlimdv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
94 52 93 impbid ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
95 94 anbi2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
96 95 exbidv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
97 96 ralbidv ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
98 97 anbi2d ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) ) )
99 98 3adant3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍 ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ 𝑀 } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) ) )
100 13 99 bitrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑒 ∈ 𝐾 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) ) )