This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlictr

Description: Graph local isomorphism is transitive. (Contributed by AV, 10-Jun-2025)

Ref Expression
Assertion grlictr ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → 𝑅 ≃𝑙𝑔𝑟 𝑇 )

Proof

Step Hyp Ref Expression
1 grlicrcl ⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) )
2 grlicrcl ⊢ ( 𝑆 ≃𝑙𝑔𝑟 𝑇 → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
3 1 2 anim12i ⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) )
4 eqid ⊢ ( Vtx ‘ 𝑅 ) = ( Vtx ‘ 𝑅 )
5 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
6 4 5 grilcbri ⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) )
7 eqid ⊢ ( Vtx ‘ 𝑇 ) = ( Vtx ‘ 𝑇 )
8 5 7 grilcbri ⊢ ( 𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) )
9 vex ⊢ ℎ ∈ V
10 vex ⊢ 𝑔 ∈ V
11 9 10 coex ⊢ ( ℎ ∘ 𝑔 ) ∈ V
12 11 a1i ⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ℎ ∘ 𝑔 ) ∈ V )
13 f1oco ⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) → ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) )
14 13 ad2ant2r ⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) )
15 f1of ⊢ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → 𝑔 : ( Vtx ‘ 𝑅 ) ⟶ ( Vtx ‘ 𝑆 ) )
16 15 ffvelcdmda ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑔 ‘ 𝑟 ) ∈ ( Vtx ‘ 𝑆 ) )
17 oveq2 ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑆 ClNeighbVtx 𝑠 ) = ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) )
18 17 oveq2d ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) = ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) )
19 fveq2 ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( ℎ ‘ 𝑠 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) )
20 19 oveq2d ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) = ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) )
21 20 oveq2d ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) )
22 18 21 breq12d ⊢ ( 𝑠 = ( 𝑔 ‘ 𝑟 ) → ( ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ↔ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) )
23 22 rspcv ⊢ ( ( 𝑔 ‘ 𝑟 ) ∈ ( Vtx ‘ 𝑆 ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) )
24 16 23 syl ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ) )
25 fvco3 ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) ⟶ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) )
26 15 25 sylan ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) = ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) )
27 26 eqcomd ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) = ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) )
28 27 oveq2d ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) = ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) )
29 28 oveq2d ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
30 29 breq2d ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ ( 𝑔 ‘ 𝑟 ) ) ) ) ↔ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
31 24 30 sylibd ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
32 31 ex ⊢ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( 𝑟 ∈ ( Vtx ‘ 𝑅 ) → ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) )
33 32 com3r ⊢ ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) → ( 𝑟 ∈ ( Vtx ‘ 𝑅 ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) )
34 33 imp31 ⊢ ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
35 34 anim1ci ⊢ ( ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) ∧ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ∧ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
36 grictr ⊢ ( ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ∧ ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
37 35 36 syl ⊢ ( ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) ∧ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
38 37 ex ⊢ ( ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) ∧ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) → ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
39 38 ralimdva ⊢ ( ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ∧ 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ) → ( ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
40 39 expimpd ⊢ ( ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
41 40 adantl ⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
42 41 imp ⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
43 14 42 jca ⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ( ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
44 f1oeq1 ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ↔ ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) )
45 fveq1 ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑓 ‘ 𝑟 ) = ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) )
46 45 oveq2d ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) = ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) )
47 46 oveq2d ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) = ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) )
48 47 breq2d ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ↔ ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
49 48 ralbidv ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ↔ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) )
50 44 49 anbi12d ⊢ ( 𝑓 = ( ℎ ∘ 𝑔 ) → ( ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ↔ ( ( ℎ ∘ 𝑔 ) : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ( ℎ ∘ 𝑔 ) ‘ 𝑟 ) ) ) ) ) )
51 12 43 50 spcedv ⊢ ( ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ∧ ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) )
52 51 ex ⊢ ( ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
53 52 exlimiv ⊢ ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
54 53 com12 ⊢ ( ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
55 54 exlimiv ⊢ ( ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) → ( ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
56 55 imp ⊢ ( ( ∃ 𝑔 ( 𝑔 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx ( 𝑔 ‘ 𝑟 ) ) ) ) ∧ ∃ ℎ ( ℎ : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑠 ∈ ( Vtx ‘ 𝑆 ) ( 𝑆 ISubGr ( 𝑆 ClNeighbVtx 𝑠 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( ℎ ‘ 𝑠 ) ) ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) )
57 6 8 56 syl2an ⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) )
58 57 adantr ⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) )
59 4 7 dfgrlic2 ⊢ ( ( 𝑅 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
60 59 ad2ant2rl ⊢ ( ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
61 60 adantl ⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → ( 𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑅 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∀ 𝑟 ∈ ( Vtx ‘ 𝑅 ) ( 𝑅 ISubGr ( 𝑅 ClNeighbVtx 𝑟 ) ) ≃𝑔𝑟 ( 𝑇 ISubGr ( 𝑇 ClNeighbVtx ( 𝑓 ‘ 𝑟 ) ) ) ) ) )
62 58 61 mpbird ⊢ ( ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) ∧ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) → 𝑅 ≃𝑙𝑔𝑟 𝑇 )
63 3 62 mpdan ⊢ ( ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇 ) → 𝑅 ≃𝑙𝑔𝑟 𝑇 )