Theorem grlictr 49386

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 49378	. . 3 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → (𝑅 ∈ V ∧ 𝑆 ∈ V))
2		grlicrcl 49378	. . 3 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → (𝑆 ∈ V ∧ 𝑇 ∈ V))
3	1, 2	anim12i 625	. 2 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)))
4		eqid 2763	. . . . . 6 ⊢ (Vtx‘𝑅) = (Vtx‘𝑅)
5		eqid 2763	. . . . . 6 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
6	4, 5	grilcbri 49380	. . . . 5 ⊢ (𝑅 ≃𝑙𝑔𝑟 𝑆 → ∃𝑔(𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))))
7		eqid 2763	. . . . . 6 ⊢ (Vtx‘𝑇) = (Vtx‘𝑇)
8	5, 7	grilcbri 49380	. . . . 5 ⊢ (𝑆 ≃𝑙𝑔𝑟 𝑇 → ∃ℎ(ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))))
9		vex 3458	. . . . . . . . . . . . 13 ⊢ ℎ ∈ V
10		vex 3458	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
11	9, 10	coex 7976	. . . . . . . . . . . 12 ⊢ (ℎ ∘ 𝑔) ∈ V
12	11	a1i 11	. . . . . . . . . . 11 ⊢ (((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → (ℎ ∘ 𝑔) ∈ V)
13		f1oco 6878	. . . . . . . . . . . . 13 ⊢ ((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ 𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆)) → (ℎ ∘ 𝑔):(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇))
14	13	ad2ant2r 760	. . . . . . . . . . . 12 ⊢ (((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → (ℎ ∘ 𝑔):(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇))
15		f1of 6854	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) → 𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆))
16	15	ffvelcdmda 7116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑔‘𝑟) ∈ (Vtx‘𝑆))
17		oveq2 7459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ClNeighbVtx 𝑠) = (𝑆 ClNeighbVtx (𝑔‘𝑟)))
18	17	oveq2d 7467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) = (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))
19		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑠 = (𝑔‘𝑟) → (ℎ‘𝑠) = (ℎ‘(𝑔‘𝑟)))
20	19	oveq2d 7467	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ClNeighbVtx (ℎ‘𝑠)) = (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))
21	20	oveq2d 7467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = (𝑔‘𝑟) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) = (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))))
22	18, 21	breq12d 5121	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = (𝑔‘𝑟) → ((𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
23	22	rspcv 3576	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔‘𝑟) ∈ (Vtx‘𝑆) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
24	16, 23	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))))))
25		fvco3 7016	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔:(Vtx‘𝑅)⟶(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
26	15, 25	sylan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((ℎ ∘ 𝑔)‘𝑟) = (ℎ‘(𝑔‘𝑟)))
27	26	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (ℎ‘(𝑔‘𝑟)) = ((ℎ ∘ 𝑔)‘𝑟))
28	27	oveq2d 7467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟))) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
29	28	oveq2d 7467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
30	29	breq2d 5120	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘(𝑔‘𝑟)))) ↔ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
31	24, 30	sylibd 242	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
32	31	ex 418	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
33	32	com3r 88	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) → (𝑟 ∈ (Vtx‘𝑅) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
34	33	imp31 423	. . . . . . . . . . . . . . . . . . 19 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
35	34	anim1ci 628	. . . . . . . . . . . . . . . . . 18 ⊢ ((((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) ∧ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ∧ (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
36		grictr 49294	. . . . . . . . . . . . . . . . . 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-1onto(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) ∧ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
38	37	ex 418	. . . . . . . . . . . . . . . 16 ⊢ (((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆)) ∧ 𝑟 ∈ (Vtx‘𝑅)) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
39	38	ralimdva 3178	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) ∧ 𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆)) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
40	39	expimpd 459	. . . . . . . . . . . . . 14 ⊢ (∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))) → ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
41	40	adantl 487	. . . . . . . . . . . . 13 ⊢ ((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) → ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
42	41	imp 412	. . . . . . . . . . . 12 ⊢ (((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
43	14, 42	jca 521	. . . . . . . . . . 11 ⊢ (((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → ((ℎ ∘ 𝑔):(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
44		f1oeq1 6842	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ↔ (ℎ ∘ 𝑔):(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇)))
45		fveq1 6915	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑓‘𝑟) = ((ℎ ∘ 𝑔)‘𝑟))
46	45	oveq2d 7467	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ClNeighbVtx (𝑓‘𝑟)) = (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))
47	46	oveq2d 7467	. . . . . . . . . . . . . 14 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) = (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))
48	47	breq2d 5120	. . . . . . . . . . . . 13 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ (𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
49	48	ralbidv 3189	. . . . . . . . . . . 12 ⊢ (𝑓 = (ℎ ∘ 𝑔) → (∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))) ↔ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟)))))
50	44, 49	anbi12d 644	. . . . . . . . . . 11 ⊢ (𝑓 = (ℎ ∘ 𝑔) → ((𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))) ↔ ((ℎ ∘ 𝑔):(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx ((ℎ ∘ 𝑔)‘𝑟))))))
51	12, 43, 50	spcedv 3556	. . . . . . . . . 10 ⊢ (((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) ∧ (𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟))))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
52	51	ex 418	. . . . . . . . 9 ⊢ ((ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) → ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
53	52	exlimiv 1965	. . . . . . . 8 ⊢ (∃ℎ(ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) → ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
54	53	com12 33	. . . . . . 7 ⊢ ((𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → (∃ℎ(ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
55	54	exlimiv 1965	. . . . . 6 ⊢ (∃𝑔(𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) → (∃ℎ(ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠)))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
56	55	imp 412	. . . . 5 ⊢ ((∃𝑔(𝑔:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑆) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑆 ISubGr (𝑆 ClNeighbVtx (𝑔‘𝑟)))) ∧ ∃ℎ(ℎ:(Vtx‘𝑆)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑠 ∈ (Vtx‘𝑆)(𝑆 ISubGr (𝑆 ClNeighbVtx 𝑠)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (ℎ‘𝑠))))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
57	6, 8, 56	syl2an 608	. . . 4 ⊢ ((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
58	57	adantr 486	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟)))))
59	4, 7	dfgrlic2 49379	. . . . 5 ⊢ ((𝑅 ∈ V ∧ 𝑇 ∈ V) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
60	59	ad2ant2rl 762	. . . 4 ⊢ (((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V)) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(Vtx‘𝑇) ∧ ∀𝑟 ∈ (Vtx‘𝑅)(𝑅 ISubGr (𝑅 ClNeighbVtx 𝑟)) ≃𝑔𝑟 (𝑇 ISubGr (𝑇 ClNeighbVtx (𝑓‘𝑟))))))
61	60	adantl 487	. . 3 ⊢ (((𝑅 ≃𝑙𝑔𝑟 𝑆 ∧ 𝑆 ≃𝑙𝑔𝑟 𝑇) ∧ ((𝑅 ∈ V ∧ 𝑆 ∈ V) ∧ (𝑆 ∈ V ∧ 𝑇 ∈ V))) → (𝑅 ≃𝑙𝑔𝑟 𝑇 ↔ ∃𝑓(𝑓:(Vtx‘𝑅)⟶1-1onto(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 2147  ∀wral 3080  Vcvv 3454   class class class wbr 5108   ∘ ccom 5662  ⟶wf 6562  ⟶1-1ontowf1o 6565  ‘cfv 6566  (class class class)co 7451  Vtxcvtx 29631   ClNeighbVtx cclnbgr 49189   ISubGr cisubgr 49231   ≃_𝑔𝑟 cgric 49247   ≃_𝑙𝑔𝑟 cgrlic 49348

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-1o 8514  df-map 8887  df-grim 49249  df-gric 49252  df-grlim 49349  df-grlic 49352

This theorem is used by:  grlicer  49387