grictr

Description: Graph isomorphism is transitive. (Contributed by AV, 5-Dec-2022) (Revised by AV, 3-May-2025)

		Ref	Expression
	Assertion	grictr	$⊢ (R ≃_{𝑔𝑟} S \land S ≃_{𝑔𝑟} T) \to R ≃_{𝑔𝑟} T$

Step	Hyp	Ref	Expression
1		brgric	$⊢ R ≃_{𝑔𝑟} S \leftrightarrow R GraphIso S \neq \emptyset$
2		brgric	$⊢ S ≃_{𝑔𝑟} T \leftrightarrow S GraphIso T \neq \emptyset$
3		n0	$⊢ R GraphIso S \neq \emptyset \leftrightarrow \exists g g \in (R GraphIso S)$
4		n0	$⊢ S GraphIso T \neq \emptyset \leftrightarrow \exists f f \in (S GraphIso T)$
5		exdistrv	$⊢ \exists g \exists f (g \in (R GraphIso S) \land f \in (S GraphIso T)) \leftrightarrow (\exists g g \in (R GraphIso S) \land \exists f f \in (S GraphIso T))$
6		grimco	$⊢ (f \in (S GraphIso T) \land g \in (R GraphIso S)) \to f \circ g \in (R GraphIso T)$
7	6	ancoms	$⊢ (g \in (R GraphIso S) \land f \in (S GraphIso T)) \to f \circ g \in (R GraphIso T)$
8		brgrici	$⊢ f \circ g \in (R GraphIso T) \to R ≃_{𝑔𝑟} T$
9	7 8	syl	$⊢ (g \in (R GraphIso S) \land f \in (S GraphIso T)) \to R ≃_{𝑔𝑟} T$
10	9	exlimivv	$⊢ \exists g \exists f (g \in (R GraphIso S) \land f \in (S GraphIso T)) \to R ≃_{𝑔𝑟} T$
11	5 10	sylbir	$⊢ (\exists g g \in (R GraphIso S) \land \exists f f \in (S GraphIso T)) \to R ≃_{𝑔𝑟} T$
12	3 4 11	syl2anb	$⊢ (R GraphIso S \neq \emptyset \land S GraphIso T \neq \emptyset) \to R ≃_{𝑔𝑟} T$
13	1 2 12	syl2anb	$⊢ (R ≃_{𝑔𝑟} S \land S ≃_{𝑔𝑟} T) \to R ≃_{𝑔𝑟} T$

Metamath Proof Explorer