ringcisoALTV

Description: An isomorphism in the category of rings is a bijection. (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ringcsectALTV.c	$⊢ C = RingCatALTV (U)$
2		ringcsectALTV.b	$⊢ B = {Base}_{C}$
3		ringcsectALTV.u	$⊢ φ \to U \in V$
4		ringcsectALTV.x	$⊢ φ \to X \in B$
5		ringcsectALTV.y	$⊢ φ \to Y \in B$
6		ringcisoALTV.n	$⊢ I = Iso (C)$
7		eqid	$⊢ Inv (C) = Inv (C)$
8	1	ringccatALTV	$⊢ 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	ringcinvALTV	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \leftrightarrow (F \in (X RingIso Y) \land (X Inv (C) Y) (F) = F^{-1}))$
16		simpl	$⊢ (F \in (X RingIso Y) \land (X Inv (C) Y) (F) = F^{-1}) \to F \in (X RingIso Y)$
17	15 16	syl6bi	$⊢ φ \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \to F \in (X RingIso Y))$
18	14 17	sylbid	$⊢ φ \to (F \in dom (X Inv (C) Y) \to F \in (X RingIso Y))$
19		eqid	$⊢ F^{-1} = F^{-1}$
20	1 2 3 4 5 7	ringcinvALTV	$⊢ φ \to (F (X Inv (C) Y) F^{-1} \leftrightarrow (F \in (X RingIso 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 RingIso Y) \land F^{-1} = F^{-1}) \to F \in dom (X Inv (C) Y))$
27	19 26	mpan2i	$⊢ φ \to (F \in (X RingIso 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 RingIso Y))$
29	11 28	bitrd	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in (X RingIso Y))$

Metamath Proof Explorer

Theorem ringcisoALTV

Proof