Theorem brcic

Description: The relation "is isomorphic to" for categories. (Contributed by AV, 5-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$$
Assertion	brcic	$$⊢\phi \to \left(X{\simeq }_{𝑐}\left(C\right)Y\leftrightarrow XIY\ne \varnothing \right)$$

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		cicfval	$$⊢C\in \mathrm{Cat}\to {\simeq }_{𝑐}\left(C\right)=\mathrm{Iso}\left(C\right)\mathrm{supp}\varnothing$$
7	3 6	syl	$$⊢\phi \to {\simeq }_{𝑐}\left(C\right)=\mathrm{Iso}\left(C\right)\mathrm{supp}\varnothing$$
8	7	breqd	$$⊢\phi \to \left(X{\simeq }_{𝑐}\left(C\right)Y\leftrightarrow X{supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)Y\right)$$
9		df-br	$$⊢X{supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)Y\leftrightarrow ⟨X,Y⟩\in {supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)$$
10	9	a1i	$$⊢\phi \to \left(X{supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)Y\leftrightarrow ⟨X,Y⟩\in {supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)\right)$$
11	1	a1i	$$⊢\phi \to I=\mathrm{Iso}\left(C\right)$$
12	11	fveq1d	$$⊢\phi \to I\left(⟨X,Y⟩\right)=\mathrm{Iso}\left(C\right)\left(⟨X,Y⟩\right)$$
13	12	neeq1d	$$⊢\phi \to \left(I\left(⟨X,Y⟩\right)\ne \varnothing \leftrightarrow \mathrm{Iso}\left(C\right)\left(⟨X,Y⟩\right)\ne \varnothing \right)$$
14		df-ov	$$⊢XIY=I\left(⟨X,Y⟩\right)$$
15	14	eqcomi	$$⊢I\left(⟨X,Y⟩\right)=XIY$$
16	15	a1i	$$⊢\phi \to I\left(⟨X,Y⟩\right)=XIY$$
17	16	neeq1d	$$⊢\phi \to \left(I\left(⟨X,Y⟩\right)\ne \varnothing \leftrightarrow XIY\ne \varnothing \right)$$
18		fvexd	$$⊢\phi \to {\mathrm{Base}}_C\in \mathrm{V}$$
19	18 18	xpexd	$$⊢\phi \to {\mathrm{Base}}_C\times {\mathrm{Base}}_C\in \mathrm{V}$$
20	4 2	eleqtrdi	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
21	5 2	eleqtrdi	$$⊢\phi \to Y\in {\mathrm{Base}}_C$$
22	20 21	opelxpd	$$⊢\phi \to ⟨X,Y⟩\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
23		isofn	$$⊢C\in \mathrm{Cat}\to \mathrm{Iso}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
24	3 23	syl	$$⊢\phi \to \mathrm{Iso}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
25		fvn0elsuppb	$$⊢\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\in \mathrm{V}\wedge ⟨X,Y⟩\in \left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\wedge \mathrm{Iso}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)\right)\to \left(\mathrm{Iso}\left(C\right)\left(⟨X,Y⟩\right)\ne \varnothing \leftrightarrow ⟨X,Y⟩\in {supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)\right)$$
26	19 22 24 25	syl3anc	$$⊢\phi \to \left(\mathrm{Iso}\left(C\right)\left(⟨X,Y⟩\right)\ne \varnothing \leftrightarrow ⟨X,Y⟩\in {supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)\right)$$
27	13 17 26	3bitr3rd	$$⊢\phi \to \left(⟨X,Y⟩\in {supp}_{\varnothing }\left(\mathrm{Iso}\left(C\right)\right)\leftrightarrow XIY\ne \varnothing \right)$$
28	8 10 27	3bitrd	$$⊢\phi \to \left(X{\simeq }_{𝑐}\left(C\right)Y\leftrightarrow XIY\ne \varnothing \right)$$