Theorem grlictr 48203

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 48195	. . 3 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → (𝑅 ∈ V ∧ 𝑆 ∈ V))
2		grlicrcl 48195	. . 3 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → (𝑆 ∈ V ∧ 𝑇 ∈ V))
3	1, 2	anim12i 613	. 2 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)))
4		eqid 2734	. . . . . 6 ⊢ (Vtx‘𝑅) = (Vtx‘𝑅)
5		eqid 2734	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
6	4, 5	grilcbri 48197	. . . . 5 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃𝑔(𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))))
7		eqid 2734	. . . . . 6 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
8	5, 7	grilcbri 48197	. . . . 5 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ℎ(ℎ:(Vtx‘𝑆)–1-1-onto→(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))))
9		vex 3442	. . . . . . . . . . . . 13 ⊢ ℎ ∈ V
10		vex 3442	. . . . . . . . . . . . 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 6795	. . . . . . . . . . . . 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 6772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) → 𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆))
16	15	ffvelcdmda 7027	. . . . . . . . . . . . . . . . . . . . . . . 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 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = (𝑔‘𝑟) → (ℎ‘𝑠) = (ℎ‘(𝑔‘𝑟)))
20	19	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ClNeighbVtx (ℎ‘𝑠)) = (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))
21	20	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) = (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))))
22	18, 21	breq12d 5109	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑔‘𝑟) → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
23	22	rspcv 3570	. . . . . . . . . . . . . . . . . . . . . . . 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 6931	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
26	15, 25	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
27	26	eqcomd 2740	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5108	. . . . . . . . . . . . . . . . . . . . . . 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 48111	. . . . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . . 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 6760	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓:(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇) ↔ (ℎ ∘ 𝑔):(Vtx‘𝑅)–1-1-onto→(Vtx‘𝑇)))
45		fveq1 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓‘𝑟) = ((ℎ ∘ 𝑔)‘𝑟))
46	45	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ClNeighbVtx (𝑓‘𝑟)) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
47	46	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
48	47	breq2d 5108	. . . . . . . . . . . . 13 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
49	48	ralbidv 3157	. . . . . . . . . . . 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 3550	. . . . . . . . . 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 1931	. . . . . . . 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 1931	. . . . . 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 48196	. . . . 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 1541  ∃wex 1780   ∈ wcel 2113  ∀wral 3049  Vcvv 3438   class class class wbr 5096   ∘ ccom 5626  ⟶wf 6486  –1-1-onto→wf1o 6489  ‘cfv 6490  (class class class)co 7356  Vtxcvtx 29018   ClNeighbVtx cclnbgr 48006   ISubGr cisubgr 48048   ≃_𝑔𝑟 cgric 48064   ≃_𝑙𝑔𝑟 cgrlic 48165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-1o 8395  df-map 8763  df-grim 48066  df-gric 48069  df-grlim 48166  df-grlic 48169

This theorem is referenced by:  grlicer  48204