gictr

Description: Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016)

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

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

Metamath Proof Explorer