Metamath Proof Explorer

Theorem cic

Description: Objects X and Y in a category are isomorphic provided that there is an isomorphism f : X --> Y , see definition 3.15 of Adamek p. 29. (Contributed by AV, 4-Apr-2020)

		Ref	Expression
	Hypotheses	cic.i	$⊢ I = Iso (C)$
		cic.b	$⊢ B = {Base}_{C}$
		cic.c	$⊢ φ \to C \in Cat$
		cic.x	$⊢ φ \to X \in B$
		cic.y	$⊢ φ \to Y \in B$
	Assertion	cic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists f f \in (X I Y))$

Proof

Step	Hyp	Ref	Expression
1		cic.i	$⊢ I = Iso (C)$
2		cic.b	$⊢ B = {Base}_{C}$
3		cic.c	$⊢ φ \to C \in Cat$
4		cic.x	$⊢ φ \to X \in B$
5		cic.y	$⊢ φ \to Y \in B$
6	1 2 3 4 5	brcic	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow X I Y \neq \emptyset)$
7		n0	$⊢ X I Y \neq \emptyset \leftrightarrow \exists f f \in (X I Y)$
8	6 7	bitrdi	$⊢ φ \to (X ≃_{𝑐} (C) Y \leftrightarrow \exists f f \in (X I Y))$