Theorem brcici

Description: Prove that two objects are isomorphic by an explicit isomorphism. (Contributed by AV, 4-Apr-2020)

	Ref	Expression
Hypotheses	cic.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
	cic.b	$$⊢B={\mathrm{Base}}_C$$
	cic.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	cic.x	$$⊢\phi \to X\in B$$
	cic.y	$$⊢\phi \to Y\in B$$
	cic.f	$$⊢\phi \to F\in \left(XIY\right)$$
Assertion	brcici	$$⊢\phi \to X{\simeq }_{𝑐}\left(C\right)Y$$

Proof

Step	Hyp	Ref	Expression
1		cic.i	$$⊢I=\mathrm{Iso}\left(C\right)$$
2		cic.b	$$⊢B={\mathrm{Base}}_C$$
3		cic.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		cic.x	$$⊢\phi \to X\in B$$
5		cic.y	$$⊢\phi \to Y\in B$$
6		cic.f	$$⊢\phi \to F\in \left(XIY\right)$$
7		eleq1	$$⊢f=F\to \left(f\in \left(XIY\right)\leftrightarrow F\in \left(XIY\right)\right)$$
8	7	spcegv	$$⊢F\in \left(XIY\right)\to \left(F\in \left(XIY\right)\to \exists ff\in \left(XIY\right)\right)$$
9	6 6 8	sylc	$$⊢\phi \to \exists ff\in \left(XIY\right)$$
10	1 2 3 4 5	cic	$$⊢\phi \to \left(X{\simeq }_{𝑐}\left(C\right)Y\leftrightarrow \exists ff\in \left(XIY\right)\right)$$
11	9 10	mpbird	$$⊢\phi \to X{\simeq }_{𝑐}\left(C\right)Y$$