Theorem grlictr 47987

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

Assertion

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

Proof of Theorem grlictr

Dummy variables 𝑓 𝑔 ℎ 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		grlicrcl 47979	. . 3 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → (𝑅 ∈ V ∧ 𝑆 ∈ V))
2		grlicrcl 47979	. . 3 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → (𝑆 ∈ V ∧ 𝑇 ∈ V))
3	1, 2	anim12i 613	. 2 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)))
4		eqid 2736	. . . . . 6 ⊢ (Vtx‘𝑅) = (Vtx‘𝑅)
5		eqid 2736	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
6	4, 5	grilcbri 47981	. . . . 5 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃𝑔(𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))))
7		eqid 2736	. . . . . 6 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
8	5, 7	grilcbri 47981	. . . . 5 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ℎ(ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))))
9		vex 3468	. . . . . . . . . . . . 13 ⊢ ℎ ∈ V
10		vex 3468	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
11	9, 10	coex 7931	. . . . . . . . . . . 12 ⊢ (ℎ ∘ 𝑔) ∈ V
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (((ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → (ℎ ∘ 𝑔) ∈ V)
13		f1oco 6846	. . . . . . . . . . . . 13 ⊢ ((ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇))
14	13	ad2ant2r 747	. . . . . . . . . . . 12 ⊢ (((ℎ:(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 6823	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → 𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆))
16	15	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑔‘𝑟) ∈ (Vtx‘𝑆))
17		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ClNeighbVtx 𝑠) = (𝑆 ClNeighbVtx (𝑔‘𝑟)))
18	17	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))
19		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = (𝑔‘𝑟) → (ℎ‘𝑠) = (ℎ‘(𝑔‘𝑟)))
20	19	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ClNeighbVtx (ℎ‘𝑠)) = (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))
21	20	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) = (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))))
22	18, 21	breq12d 5137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑔‘𝑟) → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
23	22	rspcv 3602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑟) ∈ (Vtx‘𝑆) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
24	16, 23	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
25		fvco3 6983	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
26	15, 25	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
27	26	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (ℎ‘(𝑔‘𝑟)) = ((ℎ ∘ 𝑔)‘𝑟))
28	27	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
29	28	oveq2d 7426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
30	29	breq2d 5136	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
31	24, 30	sylibd 239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
32	31	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
33	32	com3r 87	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
34	33	imp31 417	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
35	34	anim1ci 616	. . . . . . . . . . . . . . . . . 18 ⊢ ((((∀𝑠 ∈ (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 47903	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ∧ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
37	35, 36	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) ∧ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
38	37	ex 412	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
39	38	ralimdva 3153	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
40	39	expimpd 453	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
41	40	adantl 481	. . . . . . . . . . . . 13 ⊢ ((ℎ:(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 406	. . . . . . . . . . . 12 ⊢ (((ℎ:(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 511	. . . . . . . . . . 11 ⊢ (((ℎ:(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 6811	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ↔ (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇)))
45		fveq1 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓‘𝑟) = ((ℎ ∘ 𝑔)‘𝑟))
46	45	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ClNeighbVtx (𝑓‘𝑟)) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
47	46	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
48	47	breq2d 5136	. . . . . . . . . . . . 13 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
49	48	ralbidv 3164	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
50	44, 49	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑓:(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 3582	. . . . . . . . . 10 ⊢ (((ℎ:(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 412	. . . . . . . . 9 ⊢ ((ℎ:(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 1930	. . . . . . . 8 ⊢ (∃ℎ(ℎ:(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 32	. . . . . . 7 ⊢ ((𝑔:(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 1930	. . . . . 6 ⊢ (∃𝑔(𝑔:(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 406	. . . . 5 ⊢ ((∃𝑔(𝑔:(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 596	. . . 4 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
58	57	adantr 480	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
59	4, 7	dfgrlic2 47980	. . . . 5 ⊢ ((𝑅 ∈ V ∧ 𝑇 ∈ V) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
60	59	ad2ant2rl 749	. . . 4 ⊢ (((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
61	60	adantl 481	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
62	58, 61	mpbird 257	. 2 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
63	3, 62	mpdan 687	1 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∀wral 3052  Vcvv 3464   class class class wbr 5124   ∘ ccom 5663  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536  (class class class)co 7410  Vtxcvtx 28980   ClNeighbVtx cclnbgr 47799   ISubGr cisubgr 47840   ≃_𝑔𝑟 cgric 47856   ≃_𝑙𝑔𝑟 cgrlic 47956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7993  df-2nd 7994  df-1o 8485  df-map 8847  df-grim 47858  df-gric 47861  df-grlim 47957  df-grlic 47960

This theorem is referenced by:  grlicer  47988