Metamath Proof Explorer

Theorem grlictr

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

Ref Expression
Assertion grlictr ⊢ R ≃ 𝑙𝑔𝑟 S ∧ S ≃ 𝑙𝑔𝑟 T → R ≃ 𝑙𝑔𝑟 T

Proof

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