cictr

		Ref	Expression
	Assertion	cictr	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to R ≃_{𝑐} (C) T$

Proof

Step	Hyp	Ref	Expression
1		ciclcl	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to R \in {Base}_{C}$
2		cicrcl	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to S \in {Base}_{C}$
3	1 2	jca	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to (R \in {Base}_{C} \land S \in {Base}_{C})$
4	3	ex	$⊢ C \in Cat \to (R ≃_{𝑐} (C) S \to (R \in {Base}_{C} \land S \in {Base}_{C}))$
5		cicrcl	$⊢ (C \in Cat \land S ≃_{𝑐} (C) T) \to T \in {Base}_{C}$
6	5	ex	$⊢ C \in Cat \to (S ≃_{𝑐} (C) T \to T \in {Base}_{C})$
7	4 6	anim12d	$⊢ C \in Cat \to ((R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))$
8	7	3impib	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})$
9		eqid	$⊢ Iso (C) = Iso (C)$
10		eqid	$⊢ {Base}_{C} = {Base}_{C}$
11		simpl	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to C \in Cat$
12		simpll	$⊢ ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}) \to R \in {Base}_{C}$
13	12	adantl	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R \in {Base}_{C}$
14		simplr	$⊢ ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}) \to S \in {Base}_{C}$
15	14	adantl	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to S \in {Base}_{C}$
16	9 10 11 13 15	cic	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to (R ≃_{𝑐} (C) S \leftrightarrow \exists f f \in (R Iso (C) S))$
17		simprr	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to T \in {Base}_{C}$
18	9 10 11 15 17	cic	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to (S ≃_{𝑐} (C) T \leftrightarrow \exists g g \in (S Iso (C) T))$
19	16 18	anbi12d	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to ((R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \leftrightarrow (\exists f f \in (R Iso (C) S) \land \exists g g \in (S Iso (C) T)))$
20	11	adantl	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to C \in Cat$
21	13	adantl	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to R \in {Base}_{C}$
22	17	adantl	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to T \in {Base}_{C}$
23		eqid	$⊢ comp (C) = comp (C)$
24	15	adantl	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to S \in {Base}_{C}$
25		simplr	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to f \in (R Iso (C) S)$
26		simpll	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to g \in (S Iso (C) T)$
27	10 23 9 20 21 24 22 25 26	isoco	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to g (⟨R, S⟩ comp (C) T) f \in (R Iso (C) T)$
28	9 10 20 21 22 27	brcici	$⊢ ((g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \land (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}))) \to R ≃_{𝑐} (C) T$
29	28	ex	$⊢ (g \in (S Iso (C) T) \land f \in (R Iso (C) S)) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T)$
30	29	ex	$⊢ g \in (S Iso (C) T) \to (f \in (R Iso (C) S) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T))$
31	30	exlimiv	$⊢ \exists g g \in (S Iso (C) T) \to (f \in (R Iso (C) S) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T))$
32	31	com12	$⊢ f \in (R Iso (C) S) \to (\exists g g \in (S Iso (C) T) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T))$
33	32	exlimiv	$⊢ \exists f f \in (R Iso (C) S) \to (\exists g g \in (S Iso (C) T) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T))$
34	33	imp	$⊢ (\exists f f \in (R Iso (C) S) \land \exists g g \in (S Iso (C) T)) \to ((C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to R ≃_{𝑐} (C) T)$
35	34	com12	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to ((\exists f f \in (R Iso (C) S) \land \exists g g \in (S Iso (C) T)) \to R ≃_{𝑐} (C) T)$
36	19 35	sylbid	$⊢ (C \in Cat \land ((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C})) \to ((R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to R ≃_{𝑐} (C) T)$
37	36	ex	$⊢ C \in Cat \to (((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}) \to ((R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to R ≃_{𝑐} (C) T))$
38	37	com23	$⊢ C \in Cat \to ((R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to (((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}) \to R ≃_{𝑐} (C) T))$
39	38	3impib	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to (((R \in {Base}_{C} \land S \in {Base}_{C}) \land T \in {Base}_{C}) \to R ≃_{𝑐} (C) T)$
40	8 39	mpd	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S \land S ≃_{𝑐} (C) T) \to R ≃_{𝑐} (C) T$

Metamath Proof Explorer

Theorem cictr

Proof