Theorem grlictr 48840

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 48832	. . 3 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → (𝑅 ∈ V ∧ 𝑆 ∈ V))
2		grlicrcl 48832	. . 3 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → (𝑆 ∈ V ∧ 𝑇 ∈ V))
3	1, 2	anim12i 625	. 2 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)))
4		eqid 2765	. . . . . 6 ⊢ (Vtx‘𝑅) = (Vtx‘𝑅)
5		eqid 2765	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
6	4, 5	grilcbri 48834	. . . . 5 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃𝑔(𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))))
7		eqid 2765	. . . . . 6 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
8	5, 7	grilcbri 48834	. . . . 5 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ℎ(ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))))
9		vex 3461	. . . . . . . . . . . . 13 ⊢ ℎ ∈ V
10		vex 3461	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
11	9, 10	coex 7933	. . . . . . . . . . . 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 6848	. . . . . . . . . . . . 13 ⊢ ((ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇))
14	13	ad2ant2r 760	. . . . . . . . . . . 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 6824	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → 𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆))
16	15	ffvelcdmda 7083	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑔‘𝑟) ∈ (Vtx‘𝑆))
17		oveq2 7427	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ClNeighbVtx 𝑠) = (𝑆 ClNeighbVtx (𝑔‘𝑟)))
18	17	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))
19		fveq2 6885	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = (𝑔‘𝑟) → (ℎ‘𝑠) = (ℎ‘(𝑔‘𝑟)))
20	19	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ClNeighbVtx (ℎ‘𝑠)) = (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))
21	20	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) = (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))))
22	18, 21	breq12d 5124	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑔‘𝑟) → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
23	22	rspcv 3579	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑟) ∈ (Vtx‘𝑆) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
24	16, 23	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
25		fvco3 6985	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
26	15, 25	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
27	26	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (ℎ‘(𝑔‘𝑟)) = ((ℎ ∘ 𝑔)‘𝑟))
28	27	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
29	28	oveq2d 7435	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
30	29	breq2d 5123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
31	24, 30	sylibd 242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
32	31	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
33	32	com3r 88	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
34	33	imp31 423	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
35	34	anim1ci 628	. . . . . . . . . . . . . . . . . 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 48748	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ∧ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
37	35, 36	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) ∧ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
38	37	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
39	38	ralimdva 3179	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆)) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
40	39	expimpd 459	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
41	40	adantl 487	. . . . . . . . . . . . 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 412	. . . . . . . . . . . 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 521	. . . . . . . . . . 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 6812	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ↔ (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇)))
45		fveq1 6884	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓‘𝑟) = ((ℎ ∘ 𝑔)‘𝑟))
46	45	oveq2d 7435	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ClNeighbVtx (𝑓‘𝑟)) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
47	46	oveq2d 7435	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
48	47	breq2d 5123	. . . . . . . . . . . . 13 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
49	48	ralbidv 3190	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
50	44, 49	anbi12d 644	. . . . . . . . . . 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 3559	. . . . . . . . . 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 418	. . . . . . . . 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 1963	. . . . . . . 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 33	. . . . . . 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 1963	. . . . . 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 412	. . . . 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 608	. . . 4 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
58	57	adantr 486	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
59	4, 7	dfgrlic2 48833	. . . . 5 ⊢ ((𝑅 ∈ V ∧ 𝑇 ∈ V) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
60	59	ad2ant2rl 762	. . . 4 ⊢ (((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
61	60	adantl 487	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
62	58, 61	mpbird 260	. 2 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → 𝑅 ≃𝑙𝑔𝑟 𝑇)
63	3, 62	mpdan 700	1 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → 𝑅 ≃𝑙𝑔𝑟 𝑇)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3081  Vcvv 3457   class class class wbr 5111   ∘ ccom 5667  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7419  Vtxcvtx 29403   ClNeighbVtx cclnbgr 48643   ISubGr cisubgr 48685   ≃_𝑔𝑟 cgric 48701   ≃_𝑙𝑔𝑟 cgrlic 48802

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7422  df-oprab 7423  df-mpo 7424  df-1st 7992  df-2nd 7993  df-1o 8459  df-map 8832  df-grim 48703  df-gric 48706  df-grlim 48803  df-grlic 48806

This theorem is used by:  grlicer  48841