Metamath Proof Explorer

Theorem grilcbri2

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

Ref Expression
Hypotheses dfgrlic2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
dfgrlic2.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
dfgrlic3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
dfgrlic3.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
grilcbri2.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
grilcbri2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑋 ) )
grilcbri2.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
grilcbri2.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
Assertion grilcbri2 ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 dfgrlic2.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 dfgrlic3.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
4 dfgrlic3.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
5 grilcbri2.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝑋 )
6 grilcbri2.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑋 ) )
7 grilcbri2.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
8 grilcbri2.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
9 brgrlic ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ )
10 grlimdmrel ⊢ Rel dom GraphLocIso
11 10 ovprc ⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 GraphLocIso 𝐻 ) = ∅ )
12 11 necon1ai ⊢ ( ( 𝐺 GraphLocIso 𝐻 ) ≠ ∅ → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
13 9 12 sylbi ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
14 eqid ⊢ ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝑣 )
15 eqid ⊢ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) )
16 eqid ⊢ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) }
17 eqid ⊢ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) }
18 1 2 3 4 14 15 16 17 dfgrlic3 ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
19 eqidd ⊢ ( 𝑣 = 𝑋 → 𝑗 = 𝑗 )
20 oveq2 ⊢ ( 𝑣 = 𝑋 → ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝑋 ) )
21 20 5 eqtr4di ⊢ ( 𝑣 = 𝑋 → ( 𝐺 ClNeighbVtx 𝑣 ) = 𝑁 )
22 fveq2 ⊢ ( 𝑣 = 𝑋 → ( 𝑓 ‘ 𝑣 ) = ( 𝑓 ‘ 𝑋 ) )
23 22 oveq2d ⊢ ( 𝑣 = 𝑋 → ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑋 ) ) )
24 23 6 eqtr4di ⊢ ( 𝑣 = 𝑋 → ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = 𝑀 )
25 19 21 24 f1oeq123d ⊢ ( 𝑣 = 𝑋 → ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ↔ 𝑗 : 𝑁 –1-1-onto→ 𝑀 ) )
26 eqidd ⊢ ( 𝑣 = 𝑋 → 𝑔 = 𝑔 )
27 21 sseq2d ⊢ ( 𝑣 = 𝑋 → ( ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) ↔ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 ) )
28 27 rabbidv ⊢ ( 𝑣 = 𝑋 → { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } )
29 28 7 eqtr4di ⊢ ( 𝑣 = 𝑋 → { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = 𝐾 )
30 24 sseq2d ⊢ ( 𝑣 = 𝑋 → ( ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ↔ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 ) )
31 30 rabbidv ⊢ ( 𝑣 = 𝑋 → { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } )
32 31 8 eqtr4di ⊢ ( 𝑣 = 𝑋 → { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } = 𝐿 )
33 26 29 32 f1oeq123d ⊢ ( 𝑣 = 𝑋 → ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ↔ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) )
34 29 raleqdv ⊢ ( 𝑣 = 𝑋 → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
35 33 34 anbi12d ⊢ ( 𝑣 = 𝑋 → ( ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
36 35 exbidv ⊢ ( 𝑣 = 𝑋 → ( ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
37 25 36 anbi12d ⊢ ( 𝑣 = 𝑋 → ( ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
38 37 exbidv ⊢ ( 𝑣 = 𝑋 → ( ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
39 38 rspcv ⊢ ( 𝑋 ∈ 𝑉 → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
40 39 com12 ⊢ ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
41 40 a1i ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )
42 41 anim2d ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) ) )
43 42 eximdv ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ∃ 𝑗 ( 𝑗 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) ) )
44 18 43 sylbid ⊢ ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) ) )
45 13 44 mpcom ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑋 ∈ 𝑉 → ∃ 𝑗 ( 𝑗 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑗 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ) )