This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cicrcl

Description: Isomorphism implies the right side is an object. (Contributed by AV, 5-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		cicfval	$⊢ C \in Cat \to ≃_{𝑐} (C) = Iso (C) supp \emptyset$
2	1	breqd	$⊢ C \in Cat \to (R ≃_{𝑐} (C) S \leftrightarrow R {supp}_{\emptyset} (Iso (C)) S)$
3		isofn	$⊢ C \in Cat \to Iso (C) Fn ({Base}_{C} \times {Base}_{C})$
4		fvexd	$⊢ C \in Cat \to Iso (C) \in V$
5		0ex	$⊢ \emptyset \in V$
6	5	a1i	$⊢ C \in Cat \to \emptyset \in V$
7		df-br	$⊢ R {supp}_{\emptyset} (Iso (C)) S \leftrightarrow ⟨R, S⟩ \in {supp}_{\emptyset} (Iso (C))$
8		elsuppfng	$⊢ (Iso (C) Fn ({Base}_{C} \times {Base}_{C}) \land Iso (C) \in V \land \emptyset \in V) \to (⟨R, S⟩ \in {supp}_{\emptyset} (Iso (C)) \leftrightarrow (⟨R, S⟩ \in ({Base}_{C} \times {Base}_{C}) \land Iso (C) (⟨R, S⟩) \neq \emptyset))$
9	7 8	bitrid	$⊢ (Iso (C) Fn ({Base}_{C} \times {Base}_{C}) \land Iso (C) \in V \land \emptyset \in V) \to (R {supp}_{\emptyset} (Iso (C)) S \leftrightarrow (⟨R, S⟩ \in ({Base}_{C} \times {Base}_{C}) \land Iso (C) (⟨R, S⟩) \neq \emptyset))$
10	3 4 6 9	syl3anc	$⊢ C \in Cat \to (R {supp}_{\emptyset} (Iso (C)) S \leftrightarrow (⟨R, S⟩ \in ({Base}_{C} \times {Base}_{C}) \land Iso (C) (⟨R, S⟩) \neq \emptyset))$
11		opelxp2	$⊢ ⟨R, S⟩ \in ({Base}_{C} \times {Base}_{C}) \to S \in {Base}_{C}$
12	11	adantr	$⊢ (⟨R, S⟩ \in ({Base}_{C} \times {Base}_{C}) \land Iso (C) (⟨R, S⟩) \neq \emptyset) \to S \in {Base}_{C}$
13	10 12	biimtrdi	$⊢ C \in Cat \to (R {supp}_{\emptyset} (Iso (C)) S \to S \in {Base}_{C})$
14	2 13	sylbid	$⊢ C \in Cat \to (R ≃_{𝑐} (C) S \to S \in {Base}_{C})$
15	14	imp	$⊢ (C \in Cat \land R ≃_{𝑐} (C) S) \to S \in {Base}_{C}$