setcinv

Description: An inverse in the category of sets is the converse operation. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	setcmon.c	$⊢ C = SetCat (U)$
	setcmon.u	$⊢ φ \to U \in V$
	setcmon.x	$⊢ φ \to X \in U$
	setcmon.y	$⊢ φ \to Y \in U$
	setcinv.n	$⊢ N = Inv (C)$
Assertion	setcinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1}))$

Proof

Step	Hyp	Ref	Expression
1		setcmon.c	$⊢ C = SetCat (U)$
2		setcmon.u	$⊢ φ \to U \in V$
3		setcmon.x	$⊢ φ \to X \in U$
4		setcmon.y	$⊢ φ \to Y \in U$
5		setcinv.n	$⊢ N = Inv (C)$
6		eqid	$⊢ {Base}_{C} = {Base}_{C}$
7	1	setccat	$⊢ U \in V \to C \in Cat$
8	2 7	syl	$⊢ φ \to C \in Cat$
9	1 2	setcbas	$⊢ φ \to U = {Base}_{C}$
10	3 9	eleqtrd	$⊢ φ \to X \in {Base}_{C}$
11	4 9	eleqtrd	$⊢ φ \to Y \in {Base}_{C}$
12		eqid	$⊢ Sect (C) = Sect (C)$
13	6 5 8 10 11 12	isinv	$⊢ φ \to (F (X N Y) G \leftrightarrow (F (X Sect (C) Y) G \land G (Y Sect (C) X) F))$
14	1 2 3 4 12	setcsect	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}))$
15		df-3an	$⊢ (F : X ⟶ Y \land G : Y ⟶ X \land G \circ F = {I ↾}_{X}) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X})$
16	14 15	bitrdi	$⊢ φ \to (F (X Sect (C) Y) G \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X}))$
17	1 2 4 3 12	setcsect	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow (G : Y ⟶ X \land F : X ⟶ Y \land F \circ G = {I ↾}_{Y}))$
18		3ancoma	$⊢ (G : Y ⟶ X \land F : X ⟶ Y \land F \circ G = {I ↾}_{Y}) \leftrightarrow (F : X ⟶ Y \land G : Y ⟶ X \land F \circ G = {I ↾}_{Y})$
19		df-3an	$⊢ (F : X ⟶ Y \land G : Y ⟶ X \land F \circ G = {I ↾}_{Y}) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land F \circ G = {I ↾}_{Y})$
20	18 19	bitri	$⊢ (G : Y ⟶ X \land F : X ⟶ Y \land F \circ G = {I ↾}_{Y}) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land F \circ G = {I ↾}_{Y})$
21	17 20	bitrdi	$⊢ φ \to (G (Y Sect (C) X) F \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land F \circ G = {I ↾}_{Y}))$
22	16 21	anbi12d	$⊢ φ \to ((F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \leftrightarrow (((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X}) \land ((F : X ⟶ Y \land G : Y ⟶ X) \land F \circ G = {I ↾}_{Y})))$
23		anandi	$⊢ ((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y})) \leftrightarrow (((F : X ⟶ Y \land G : Y ⟶ X) \land G \circ F = {I ↾}_{X}) \land ((F : X ⟶ Y \land G : Y ⟶ X) \land F \circ G = {I ↾}_{Y}))$
24	22 23	bitr4di	$⊢ φ \to ((F (X Sect (C) Y) G \land G (Y Sect (C) X) F) \leftrightarrow ((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y})))$
25		fcof1o	$⊢ ((F : X ⟶ Y \land G : Y ⟶ X) \land (F \circ G = {I ↾}_{Y} \land G \circ F = {I ↾}_{X})) \to (F : X \underset{1-1 onto}{⟶} Y \land F^{-1} = G)$
26		eqcom	$⊢ F^{-1} = G \leftrightarrow G = F^{-1}$
27	26	anbi2i	$⊢ (F : X \underset{1-1 onto}{⟶} Y \land F^{-1} = G) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})$
28	25 27	sylib	$⊢ ((F : X ⟶ Y \land G : Y ⟶ X) \land (F \circ G = {I ↾}_{Y} \land G \circ F = {I ↾}_{X})) \to (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})$
29	28	ancom2s	$⊢ ((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y})) \to (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})$
30	29	adantl	$⊢ (φ \land ((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y}))) \to (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})$
31		f1of	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F : X ⟶ Y$
32	31	ad2antrl	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F : X ⟶ Y$
33		f1ocnv	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
34	33	ad2antrl	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F^{-1} : Y \underset{1-1 onto}{⟶} X$
35		f1oeq1	$⊢ G = F^{-1} \to (G : Y \underset{1-1 onto}{⟶} X \leftrightarrow F^{-1} : Y \underset{1-1 onto}{⟶} X)$
36	35	ad2antll	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to (G : Y \underset{1-1 onto}{⟶} X \leftrightarrow F^{-1} : Y \underset{1-1 onto}{⟶} X)$
37	34 36	mpbird	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to G : Y \underset{1-1 onto}{⟶} X$
38		f1of	$⊢ G : Y \underset{1-1 onto}{⟶} X \to G : Y ⟶ X$
39	37 38	syl	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to G : Y ⟶ X$
40		simprr	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to G = F^{-1}$
41	40	coeq1d	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to G \circ F = F^{-1} \circ F$
42		f1ococnv1	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F^{-1} \circ F = {I ↾}_{X}$
43	42	ad2antrl	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F^{-1} \circ F = {I ↾}_{X}$
44	41 43	eqtrd	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to G \circ F = {I ↾}_{X}$
45	40	coeq2d	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F \circ G = F \circ F^{-1}$
46		f1ococnv2	$⊢ F : X \underset{1-1 onto}{⟶} Y \to F \circ F^{-1} = {I ↾}_{Y}$
47	46	ad2antrl	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F \circ F^{-1} = {I ↾}_{Y}$
48	45 47	eqtrd	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to F \circ G = {I ↾}_{Y}$
49	44 48	jca	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y})$
50	32 39 49	jca31	$⊢ (φ \land (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1})) \to ((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y}))$
51	30 50	impbida	$⊢ φ \to (((F : X ⟶ Y \land G : Y ⟶ X) \land (G \circ F = {I ↾}_{X} \land F \circ G = {I ↾}_{Y})) \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1}))$
52	13 24 51	3bitrd	$⊢ φ \to (F (X N Y) G \leftrightarrow (F : X \underset{1-1 onto}{⟶} Y \land G = F^{-1}))$

Metamath Proof Explorer

Theorem setcinv

Proof