Metamath Proof Explorer

Theorem grlicsym

Description: Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Assertion grlicsym ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
3 1 2 grilcbri ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝑆 → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) )
4 grlicrcl ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝑆 → ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) )
5 vex ⊢ 𝑓 ∈ V
6 cnvexg ⊢ ( 𝑓 ∈ V → ◡ 𝑓 ∈ V )
7 5 6 mp1i ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ◡ 𝑓 ∈ V )
8 f1ocnv ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ◡ 𝑓 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) )
9 8 ad2antrr ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ◡ 𝑓 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) )
10 f1ocnvdm ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ) → ( ◡ 𝑓 ‘ 𝑤 ) ∈ ( Vtx ‘ 𝐺 ) )
11 10 3adant3 ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ◡ 𝑓 ‘ 𝑤 ) ∈ ( Vtx ‘ 𝐺 ) )
12 oveq2 ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) )
13 12 oveq2d ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) = ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) )
14 fveq2 ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( 𝑓 ‘ 𝑣 ) = ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) )
15 14 oveq2d ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) )
16 15 oveq2d ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) = ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
17 13 16 breq12d ⊢ ( 𝑣 = ( ◡ 𝑓 ‘ 𝑤 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) )
18 17 rspcv ⊢ ( ( ◡ 𝑓 ‘ 𝑤 ) ∈ ( Vtx ‘ 𝐺 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) )
19 11 18 syl ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) )
20 f1ocnvfv2 ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) = 𝑤 )
21 20 3adant3 ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) = 𝑤 )
22 21 oveq2d ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) = ( 𝑆 ClNeighbVtx 𝑤 ) )
23 22 oveq2d ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) = ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) )
24 23 breq2d ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ) )
25 simp3 ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → 𝐺 ∈ UHGraph )
26 1 clnbgrssvtx ⊢ ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ⊆ ( Vtx ‘ 𝐺 )
27 1 isubgruhgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ⊆ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ∈ UHGraph )
28 25 26 27 sylancl ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ∈ UHGraph )
29 gricsym ⊢ ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ∈ UHGraph → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
30 28 29 syl ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
31 24 30 sylbid ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
32 19 31 syld ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ∧ 𝐺 ∈ UHGraph ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
33 32 3exp ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( 𝑤 ∈ ( Vtx ‘ 𝑆 ) → ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) ) )
34 33 com24 ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) → ( 𝐺 ∈ UHGraph → ( 𝑤 ∈ ( Vtx ‘ 𝑆 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) ) )
35 34 imp31 ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ( 𝑤 ∈ ( Vtx ‘ 𝑆 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
36 35 ralrimiv ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) )
37 9 36 jca ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ( ◡ 𝑓 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
38 f1oeq1 ⊢ ( 𝑔 = ◡ 𝑓 → ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ↔ ◡ 𝑓 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ) )
39 fveq1 ⊢ ( 𝑔 = ◡ 𝑓 → ( 𝑔 ‘ 𝑤 ) = ( ◡ 𝑓 ‘ 𝑤 ) )
40 39 oveq2d ⊢ ( 𝑔 = ◡ 𝑓 → ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) = ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) )
41 40 oveq2d ⊢ ( 𝑔 = ◡ 𝑓 → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) = ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) )
42 41 breq2d ⊢ ( 𝑔 = ◡ 𝑓 → ( ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ↔ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
43 42 ralbidv ⊢ ( 𝑔 = ◡ 𝑓 → ( ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ↔ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) )
44 38 43 anbi12d ⊢ ( 𝑔 = ◡ 𝑓 → ( ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) ↔ ( ◡ 𝑓 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( ◡ 𝑓 ‘ 𝑤 ) ) ) ) ) )
45 7 37 44 spcedv ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ) → ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) )
46 45 3adant3 ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) ) → ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) )
47 2 1 dfgrlic2 ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑆 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) ) )
48 47 ancoms ⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑆 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) ) )
49 48 3ad2ant3 ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) ) → ( 𝑆 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑤 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑤 ) ) ≃𝑔𝑟 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx ( 𝑔 ‘ 𝑤 ) ) ) ) ) )
50 46 49 mpbird ⊢ ( ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ∧ 𝐺 ∈ UHGraph ∧ ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) ) → 𝑆 ≃𝑙𝑔𝑟 𝐺 )
51 50 3exp ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) → ( 𝐺 ∈ UHGraph → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) ) )
52 51 com23 ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐺 ∈ UHGraph → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) ) )
53 52 exlimiv ⊢ ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) → ( ( 𝐺 ∈ V ∧ 𝑆 ∈ V ) → ( 𝐺 ∈ UHGraph → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) ) )
54 3 4 53 sylc ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝑆 → ( 𝐺 ∈ UHGraph → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) )
55 54 com12 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑙𝑔𝑟 𝑆 → 𝑆 ≃𝑙𝑔𝑟 𝐺 ) )