rngciso

Description: An isomorphism in the category of non-unital rings is a bijection. (Contributed by AV, 28-Feb-2020)

	Ref	Expression
Hypotheses	rngcsect.c	$⊢ C = RngCat (U)$
	rngcsect.b	$⊢ B = {Base}_{C}$
	rngcsect.u	$⊢ φ \to U \in V$
	rngcsect.x	$⊢ φ \to X \in B$
	rngcsect.y	$⊢ φ \to Y \in B$
	rngciso.n	$⊢ I = Iso (C)$
Assertion	rngciso	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in (X RngIso Y))$

Proof

Step	Hyp	Ref	Expression
1		rngcsect.c	$⊢ C = RngCat (U)$
2		rngcsect.b	$⊢ B = {Base}_{C}$
3		rngcsect.u	$⊢ φ \to U \in V$
4		rngcsect.x	$⊢ φ \to X \in B$
5		rngcsect.y	$⊢ φ \to Y \in B$
6		rngciso.n	$⊢ I = Iso (C)$
7		eqid	$⊢ Inv (C) = Inv (C)$
8	1	rngccat	$⊢ U \in V \to C \in Cat$
9	3 8	syl	$⊢ φ \to C \in Cat$
10	2 7 9 4 5 6	isoval	$⊢ φ \to X I Y = dom (X Inv (C) Y)$
11	10	eleq2d	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in dom (X Inv (C) Y))$
12	2 7 9 4 5	invfun	$⊢ φ \to Fun (X Inv (C) Y)$
13		funfvbrb	$⊢ Fun (X Inv (C) Y) \to (F \in dom (X Inv (C) Y) \leftrightarrow F (X Inv (C) Y) (X Inv (C) Y) (F))$
14	12 13	syl	$⊢ φ \to (F \in dom (X Inv (C) Y) \leftrightarrow F (X Inv (C) Y) (X Inv (C) Y) (F))$
15	1 2 3 4 5 7	rngcinv	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \leftrightarrow (F \in (X RngIso Y) \land (X Inv (C) Y) (F) = F^{-1}))$
16		simpl	$⊢ (F \in (X RngIso Y) \land (X Inv (C) Y) (F) = F^{-1}) \to F \in (X RngIso Y)$
17	15 16	syl6bi	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \to F \in (X RngIso Y))$
18	14 17	sylbid	$⊢ φ \to (F \in dom (X Inv (C) Y) \to F \in (X RngIso Y))$
19		eqid	$⊢ F^{-1} = F^{-1}$
20	1 2 3 4 5 7	rngcinv	$⊢ φ \to (F (X Inv (C) Y) F^{-1} \leftrightarrow (F \in (X RngIso Y) \land F^{-1} = F^{-1}))$
21		funrel	$⊢ Fun (X Inv (C) Y) \to Rel (X Inv (C) Y)$
22	12 21	syl	$⊢ φ \to Rel (X Inv (C) Y)$
23		releldm	$⊢ (Rel (X Inv (C) Y) \land F (X Inv (C) Y) F^{-1}) \to F \in dom (X Inv (C) Y)$
24	23	ex	$⊢ Rel (X Inv (C) Y) \to (F (X Inv (C) Y) F^{-1} \to F \in dom (X Inv (C) Y))$
25	22 24	syl	$⊢ φ \to (F (X Inv (C) Y) F^{-1} \to F \in dom (X Inv (C) Y))$
26	20 25	sylbird	$⊢ φ \to ((F \in (X RngIso Y) \land F^{-1} = F^{-1}) \to F \in dom (X Inv (C) Y))$
27	19 26	mpan2i	$⊢ φ \to (F \in (X RngIso Y) \to F \in dom (X Inv (C) Y))$
28	18 27	impbid	$⊢ φ \to (F \in dom (X Inv (C) Y) \leftrightarrow F \in (X RngIso Y))$
29	11 28	bitrd	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in (X RngIso Y))$

Metamath Proof Explorer

Theorem rngciso

Proof