Theorem grlictr 48506

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 48498	. . 3 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → (𝑅 ∈ V ∧ 𝑆 ∈ V))
2		grlicrcl 48498	. . 3 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → (𝑆 ∈ V ∧ 𝑇 ∈ V))
3	1, 2	anim12i 619	. 2 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)))
4		eqid 2739	. . . . . 6 ⊢ (Vtx‘𝑅) = (Vtx‘𝑅)
5		eqid 2739	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
6	4, 5	grilcbri 48500	. . . . 5 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃𝑔(𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))))
7		eqid 2739	. . . . . 6 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
8	5, 7	grilcbri 48500	. . . . 5 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ℎ(ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))))
9		vex 3435	. . . . . . . . . . . . 13 ⊢ ℎ ∈ V
10		vex 3435	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
11	9, 10	coex 7870	. . . . . . . . . . . 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 6790	. . . . . . . . . . . . 13 ⊢ ((ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇))
14	13	ad2ant2r 753	. . . . . . . . . . . 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 6767	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → 𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆))
16	15	ffvelcdmda 7025	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑔‘𝑟) ∈ (Vtx‘𝑆))
17		oveq2 7364	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ClNeighbVtx 𝑠) = (𝑆 ClNeighbVtx (𝑔‘𝑟)))
18	17	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))
19		fveq2 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = (𝑔‘𝑟) → (ℎ‘𝑠) = (ℎ‘(𝑔‘𝑟)))
20	19	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ClNeighbVtx (ℎ‘𝑠)) = (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))
21	20	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) = (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))))
22	18, 21	breq12d 5085	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑔‘𝑟) → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
23	22	rspcv 3556	. . . . . . . . . . . . . . . . . . . . . . . 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 6927	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
26	15, 25	sylan 586	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
27	26	eqcomd 2745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (ℎ‘(𝑔‘𝑟)) = ((ℎ ∘ 𝑔)‘𝑟))
28	27	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
29	28	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
30	29	breq2d 5084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
31	24, 30	sylibd 240	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
32	31	ex 413	. . . . . . . . . . . . . . . . . . . . 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 418	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
35	34	anim1ci 622	. . . . . . . . . . . . . . . . . 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 48414	. . . . . . . . . . . . . . . . . 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 413	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
39	38	ralimdva 3151	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
40	39	expimpd 454	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
41	40	adantl 482	. . . . . . . . . . . . 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 407	. . . . . . . . . . . 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 516	. . . . . . . . . . 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 6755	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ↔ (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇)))
45		fveq1 6826	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓‘𝑟) = ((ℎ ∘ 𝑔)‘𝑟))
46	45	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ClNeighbVtx (𝑓‘𝑟)) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
47	46	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
48	47	breq2d 5084	. . . . . . . . . . . . 13 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
49	48	ralbidv 3162	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
50	44, 49	anbi12d 638	. . . . . . . . . . 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 3536	. . . . . . . . . 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 413	. . . . . . . . 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 1937	. . . . . . . 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 1937	. . . . . 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 407	. . . . 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 602	. . . 4 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
58	57	adantr 481	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
59	4, 7	dfgrlic2 48499	. . . . 5 ⊢ ((𝑅 ∈ V ∧ 𝑇 ∈ V) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
60	59	ad2ant2rl 755	. . . 4 ⊢ (((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
61	60	adantl 482	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
62	58, 61	mpbird 258	. 2 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
63	3, 62	mpdan 693	1 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∀wral 3053  Vcvv 3431   class class class wbr 5072   ∘ ccom 5622  ⟶wf 6481  –1-1-onto→wf1o 6484  ‘cfv 6485  (class class class)co 7356  Vtxcvtx 29083   ClNeighbVtx cclnbgr 48309   ISubGr cisubgr 48351   ≃_𝑔𝑟 cgric 48367   ≃_𝑙𝑔𝑟 cgrlic 48468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-1o 8395  df-map 8765  df-grim 48369  df-gric 48372  df-grlim 48469  df-grlic 48472

This theorem is referenced by:  grlicer  48507