catciso

Description: A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in Adamek p. 34. (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	catciso.c	$⊢ C = CatCat (U)$
	catciso.b	$⊢ B = {Base}_{C}$
	catciso.r	$⊢ R = {Base}_{X}$
	catciso.s	$⊢ S = {Base}_{Y}$
	catciso.u	$⊢ φ \to U \in V$
	catciso.x	$⊢ φ \to X \in B$
	catciso.y	$⊢ φ \to Y \in B$
	catciso.i	$⊢ I = Iso (C)$
Assertion	catciso	$⊢ φ \to (F \in (X I Y) \leftrightarrow (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S))$

Proof

Step	Hyp	Ref	Expression
1		catciso.c	$⊢ C = CatCat (U)$
2		catciso.b	$⊢ B = {Base}_{C}$
3		catciso.r	$⊢ R = {Base}_{X}$
4		catciso.s	$⊢ S = {Base}_{Y}$
5		catciso.u	$⊢ φ \to U \in V$
6		catciso.x	$⊢ φ \to X \in B$
7		catciso.y	$⊢ φ \to Y \in B$
8		catciso.i	$⊢ I = Iso (C)$
9		relfunc	$⊢ Rel (X Func Y)$
10		eqid	$⊢ Inv (C) = Inv (C)$
11	1	catccat	$⊢ U \in V \to C \in Cat$
12	5 11	syl	$⊢ φ \to C \in Cat$
13	2 10 12 6 7 8	isoval	$⊢ φ \to X I Y = dom (X Inv (C) Y)$
14	13	eleq2d	$⊢ φ \to (F \in (X I Y) \leftrightarrow F \in dom (X Inv (C) Y))$
15	14	biimpa	$⊢ (φ \land F \in (X I Y)) \to F \in dom (X Inv (C) Y)$
16	12	adantr	$⊢ (φ \land F \in (X I Y)) \to C \in Cat$
17	6	adantr	$⊢ (φ \land F \in (X I Y)) \to X \in B$
18	7	adantr	$⊢ (φ \land F \in (X I Y)) \to Y \in B$
19	2 10 16 17 18	invfun	$⊢ (φ \land F \in (X I Y)) \to Fun (X Inv (C) Y)$
20		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))$
21	19 20	syl	$⊢ (φ \land F \in (X I Y)) \to (F \in dom (X Inv (C) Y) \leftrightarrow F (X Inv (C) Y) (X Inv (C) Y) (F))$
22	15 21	mpbid	$⊢ (φ \land F \in (X I Y)) \to F (X Inv (C) Y) (X Inv (C) Y) (F)$
23		eqid	$⊢ Sect (C) = Sect (C)$
24	2 10 16 17 18 23	isinv	$⊢ (φ \land F \in (X I Y)) \to (F (X Inv (C) Y) (X Inv (C) Y) (F) \leftrightarrow (F (X Sect (C) Y) (X Inv (C) Y) (F) \land (X Inv (C) Y) (F) (Y Sect (C) X) F))$
25	22 24	mpbid	$⊢ (φ \land F \in (X I Y)) \to (F (X Sect (C) Y) (X Inv (C) Y) (F) \land (X Inv (C) Y) (F) (Y Sect (C) X) F)$
26	25	simpld	$⊢ (φ \land F \in (X I Y)) \to F (X Sect (C) Y) (X Inv (C) Y) (F)$
27		eqid	$⊢ Hom (C) = Hom (C)$
28		eqid	$⊢ comp (C) = comp (C)$
29		eqid	$⊢ Id (C) = Id (C)$
30	2 27 28 29 23 16 17 18	issect	$⊢ (φ \land F \in (X I Y)) \to (F (X Sect (C) Y) (X Inv (C) Y) (F) \leftrightarrow (F \in (X Hom (C) Y) \land (X Inv (C) Y) (F) \in (Y Hom (C) X) \land (X Inv (C) Y) (F) (⟨X, Y⟩ comp (C) X) F = Id (C) (X)))$
31	26 30	mpbid	$⊢ (φ \land F \in (X I Y)) \to (F \in (X Hom (C) Y) \land (X Inv (C) Y) (F) \in (Y Hom (C) X) \land (X Inv (C) Y) (F) (⟨X, Y⟩ comp (C) X) F = Id (C) (X))$
32	31	simp1d	$⊢ (φ \land F \in (X I Y)) \to F \in (X Hom (C) Y)$
33	1 2 5 27 6 7	catchom	$⊢ φ \to X Hom (C) Y = X Func Y$
34	33	adantr	$⊢ (φ \land F \in (X I Y)) \to X Hom (C) Y = X Func Y$
35	32 34	eleqtrd	$⊢ (φ \land F \in (X I Y)) \to F \in (X Func Y)$
36		1st2nd	$⊢ (Rel (X Func Y) \land F \in (X Func Y)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
37	9 35 36	sylancr	$⊢ (φ \land F \in (X I Y)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
38		1st2ndbr	$⊢ (Rel (X Func Y) \land F \in (X Func Y)) \to 1^{st} (F) (X Func Y) 2^{nd} (F)$
39	9 35 38	sylancr	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F) (X Func Y) 2^{nd} (F)$
40		eqid	$⊢ Hom (X) = Hom (X)$
41		eqid	$⊢ Hom (Y) = Hom (Y)$
42	39	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (X Func Y) 2^{nd} (F)$
43		simprl	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to x \in R$
44		simprr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to y \in R$
45	3 40 41 42 43 44	funcf2	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (x 2^{nd} (F) y) : x Hom (X) y ⟶ 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y)$
46		relfunc	$⊢ Rel (Y Func X)$
47	31	simp2d	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) \in (Y Hom (C) X)$
48	1 2 5 27 7 6	catchom	$⊢ φ \to Y Hom (C) X = Y Func X$
49	48	adantr	$⊢ (φ \land F \in (X I Y)) \to Y Hom (C) X = Y Func X$
50	47 49	eleqtrd	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) \in (Y Func X)$
51		1st2ndbr	$⊢ (Rel (Y Func X) \land (X Inv (C) Y) (F) \in (Y Func X)) \to 1^{st} ((X Inv (C) Y) (F)) (Y Func X) 2^{nd} ((X Inv (C) Y) (F))$
52	46 50 51	sylancr	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ((X Inv (C) Y) (F)) (Y Func X) 2^{nd} ((X Inv (C) Y) (F))$
53	52	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F)) (Y Func X) 2^{nd} ((X Inv (C) Y) (F))$
54	3 4 42	funcf1	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) : R ⟶ S$
55	54 43	ffvelcdmd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (x) \in S$
56	54 44	ffvelcdmd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (y) \in S$
57	4 41 40 53 55 56	funcf2	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y) ⟶ 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) Hom (X) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y))$
58	31	simp3d	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) (⟨X, Y⟩ comp (C) X) F = Id (C) (X)$
59	5	adantr	$⊢ (φ \land F \in (X I Y)) \to U \in V$
60	1 2 59 28 17 18 17 35 50	catcco	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) (⟨X, Y⟩ comp (C) X) F = (X Inv (C) Y) (F) \circ_{func} F$
61		eqid	$⊢ {id}_{func} (X) = {id}_{func} (X)$
62	1 2 29 61 5 6	catcid	$⊢ φ \to Id (C) (X) = {id}_{func} (X)$
63	62	adantr	$⊢ (φ \land F \in (X I Y)) \to Id (C) (X) = {id}_{func} (X)$
64	58 60 63	3eqtr3d	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) \circ_{func} F = {id}_{func} (X)$
65	64	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (X Inv (C) Y) (F) \circ_{func} F = {id}_{func} (X)$
66	65	fveq2d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) = 1^{st} ({id}_{func} (X))$
67	66	fveq1d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) (x) = 1^{st} ({id}_{func} (X)) (x)$
68	35	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to F \in (X Func Y)$
69	50	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (X Inv (C) Y) (F) \in (Y Func X)$
70	3 68 69 43	cofu1	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) (x) = 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x))$
71	1 2 5	catcbas	$⊢ φ \to B = U \cap Cat$
72		inss2	$⊢ U \cap Cat \subseteq Cat$
73	71 72	eqsstrdi	$⊢ φ \to B \subseteq Cat$
74	73 6	sseldd	$⊢ φ \to X \in Cat$
75	74	ad2antrr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to X \in Cat$
76	61 3 75 43	idfu1	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ({id}_{func} (X)) (x) = x$
77	67 70 76	3eqtr3d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) = x$
78	66	fveq1d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) (y) = 1^{st} ({id}_{func} (X)) (y)$
79	3 68 69 44	cofu1	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) (y) = 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y))$
80	61 3 75 44	idfu1	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ({id}_{func} (X)) (y) = y$
81	78 79 80	3eqtr3d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y)) = y$
82	77 81	oveq12d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) Hom (X) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y)) = x Hom (X) y$
83	82	feq3d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to ((1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y) ⟶ 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) Hom (X) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y)) \leftrightarrow (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y) ⟶ x Hom (X) y)$
84	57 83	mpbid	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y) ⟶ x Hom (X) y$
85	65	fveq2d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 2^{nd} ((X Inv (C) Y) (F) \circ_{func} F) = 2^{nd} ({id}_{func} (X))$
86	85	oveqd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to x 2^{nd} ((X Inv (C) Y) (F) \circ_{func} F) y = x 2^{nd} ({id}_{func} (X)) y$
87	3 68 69 43 44	cofu2nd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to x 2^{nd} ((X Inv (C) Y) (F) \circ_{func} F) y = (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)$
88	61 3 75 40 43 44	idfu2nd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to x 2^{nd} ({id}_{func} (X)) y = {I ↾}_{(x Hom (X) y)}$
89	86 87 88	3eqtr3d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y) = {I ↾}_{(x Hom (X) y)}$
90	25	simprd	$⊢ (φ \land F \in (X I Y)) \to (X Inv (C) Y) (F) (Y Sect (C) X) F$
91	2 27 28 29 23 16 18 17	issect	$⊢ (φ \land F \in (X I Y)) \to ((X Inv (C) Y) (F) (Y Sect (C) X) F \leftrightarrow ((X Inv (C) Y) (F) \in (Y Hom (C) X) \land F \in (X Hom (C) Y) \land F (⟨Y, X⟩ comp (C) Y) (X Inv (C) Y) (F) = Id (C) (Y)))$
92	90 91	mpbid	$⊢ (φ \land F \in (X I Y)) \to ((X Inv (C) Y) (F) \in (Y Hom (C) X) \land F \in (X Hom (C) Y) \land F (⟨Y, X⟩ comp (C) Y) (X Inv (C) Y) (F) = Id (C) (Y))$
93	92	simp3d	$⊢ (φ \land F \in (X I Y)) \to F (⟨Y, X⟩ comp (C) Y) (X Inv (C) Y) (F) = Id (C) (Y)$
94	1 2 59 28 18 17 18 50 35	catcco	$⊢ (φ \land F \in (X I Y)) \to F (⟨Y, X⟩ comp (C) Y) (X Inv (C) Y) (F) = F \circ_{func} (X Inv (C) Y) (F)$
95		eqid	$⊢ {id}_{func} (Y) = {id}_{func} (Y)$
96	1 2 29 95 5 7	catcid	$⊢ φ \to Id (C) (Y) = {id}_{func} (Y)$
97	96	adantr	$⊢ (φ \land F \in (X I Y)) \to Id (C) (Y) = {id}_{func} (Y)$
98	93 94 97	3eqtr3d	$⊢ (φ \land F \in (X I Y)) \to F \circ_{func} (X Inv (C) Y) (F) = {id}_{func} (Y)$
99	98	adantr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to F \circ_{func} (X Inv (C) Y) (F) = {id}_{func} (Y)$
100	99	fveq2d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 2^{nd} (F \circ_{func} (X Inv (C) Y) (F)) = 2^{nd} ({id}_{func} (Y))$
101	100	oveqd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (x) 2^{nd} (F \circ_{func} (X Inv (C) Y) (F)) 1^{st} (F) (y) = 1^{st} (F) (x) 2^{nd} ({id}_{func} (Y)) 1^{st} (F) (y)$
102	4 69 68 55 56	cofu2nd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (x) 2^{nd} (F \circ_{func} (X Inv (C) Y) (F)) 1^{st} (F) (y) = (1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) 2^{nd} (F) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y))) \circ (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y))$
103	77 81	oveq12d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) 2^{nd} (F) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y)) = x 2^{nd} (F) y$
104	103	coeq1d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (x)) 2^{nd} (F) 1^{st} ((X Inv (C) Y) (F)) (1^{st} (F) (y))) \circ (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) = (x 2^{nd} (F) y) \circ (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y))$
105	102 104	eqtrd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (x) 2^{nd} (F \circ_{func} (X Inv (C) Y) (F)) 1^{st} (F) (y) = (x 2^{nd} (F) y) \circ (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y))$
106	73	ad2antrr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to B \subseteq Cat$
107	7	ad2antrr	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to Y \in B$
108	106 107	sseldd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to Y \in Cat$
109	95 4 108 41 55 56	idfu2nd	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to 1^{st} (F) (x) 2^{nd} ({id}_{func} (Y)) 1^{st} (F) (y) = {I ↾}_{(1^{st} (F) (x) Hom (Y) 1^{st} (F) (y))}$
110	101 105 109	3eqtr3d	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (x 2^{nd} (F) y) \circ (1^{st} (F) (x) 2^{nd} ((X Inv (C) Y) (F)) 1^{st} (F) (y)) = {I ↾}_{(1^{st} (F) (x) Hom (Y) 1^{st} (F) (y))}$
111	45 84 89 110	fcof1od	$⊢ ((φ \land F \in (X I Y)) \land (x \in R \land y \in R)) \to (x 2^{nd} (F) y) : x Hom (X) y \underset{1-1 onto}{⟶} 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y)$
112	111	ralrimivva	$⊢ (φ \land F \in (X I Y)) \to \forall x \in R \forall y \in R (x 2^{nd} (F) y) : x Hom (X) y \underset{1-1 onto}{⟶} 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y)$
113	3 40 41	isffth2	$⊢ 1^{st} (F) ((X Full Y) \cap (X Faith Y)) 2^{nd} (F) \leftrightarrow (1^{st} (F) (X Func Y) 2^{nd} (F) \land \forall x \in R \forall y \in R (x 2^{nd} (F) y) : x Hom (X) y \underset{1-1 onto}{⟶} 1^{st} (F) (x) Hom (Y) 1^{st} (F) (y))$
114	39 112 113	sylanbrc	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F) ((X Full Y) \cap (X Faith Y)) 2^{nd} (F)$
115		df-br	$⊢ 1^{st} (F) ((X Full Y) \cap (X Faith Y)) 2^{nd} (F) \leftrightarrow ⟨1^{st} (F), 2^{nd} (F)⟩ \in ((X Full Y) \cap (X Faith Y))$
116	114 115	sylib	$⊢ (φ \land F \in (X I Y)) \to ⟨1^{st} (F), 2^{nd} (F)⟩ \in ((X Full Y) \cap (X Faith Y))$
117	37 116	eqeltrd	$⊢ (φ \land F \in (X I Y)) \to F \in ((X Full Y) \cap (X Faith Y))$
118	3 4 39	funcf1	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F) : R ⟶ S$
119	4 3 52	funcf1	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ((X Inv (C) Y) (F)) : S ⟶ R$
120	64	fveq2d	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) = 1^{st} ({id}_{func} (X))$
121	3 35 50	cofu1st	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ((X Inv (C) Y) (F) \circ_{func} F) = 1^{st} ((X Inv (C) Y) (F)) \circ 1^{st} (F)$
122	74	adantr	$⊢ (φ \land F \in (X I Y)) \to X \in Cat$
123	61 3 122	idfu1st	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ({id}_{func} (X)) = {I ↾}_{R}$
124	120 121 123	3eqtr3d	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ((X Inv (C) Y) (F)) \circ 1^{st} (F) = {I ↾}_{R}$
125	98	fveq2d	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F \circ_{func} (X Inv (C) Y) (F)) = 1^{st} ({id}_{func} (Y))$
126	4 50 35	cofu1st	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F \circ_{func} (X Inv (C) Y) (F)) = 1^{st} (F) \circ 1^{st} ((X Inv (C) Y) (F))$
127	73 7	sseldd	$⊢ φ \to Y \in Cat$
128	127	adantr	$⊢ (φ \land F \in (X I Y)) \to Y \in Cat$
129	95 4 128	idfu1st	$⊢ (φ \land F \in (X I Y)) \to 1^{st} ({id}_{func} (Y)) = {I ↾}_{S}$
130	125 126 129	3eqtr3d	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F) \circ 1^{st} ((X Inv (C) Y) (F)) = {I ↾}_{S}$
131	118 119 124 130	fcof1od	$⊢ (φ \land F \in (X I Y)) \to 1^{st} (F) : R \underset{1-1 onto}{⟶} S$
132	117 131	jca	$⊢ (φ \land F \in (X I Y)) \to (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)$
133	12	adantr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to C \in Cat$
134	6	adantr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to X \in B$
135	7	adantr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to Y \in B$
136		inss1	$⊢ (X Full Y) \cap (X Faith Y) \subseteq X Full Y$
137		fullfunc	$⊢ X Full Y \subseteq X Func Y$
138	136 137	sstri	$⊢ (X Full Y) \cap (X Faith Y) \subseteq X Func Y$
139		simprl	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to F \in ((X Full Y) \cap (X Faith Y))$
140	138 139	sselid	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to F \in (X Func Y)$
141	9 140 36	sylancr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
142	5	adantr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to U \in V$
143		eqid	$⊢ (x \in S, y \in S ⟼ {({1^{st} (F)}^{-1} (x) 2^{nd} (F) {1^{st} (F)}^{-1} (y))}^{-1}) = (x \in S, y \in S ⟼ {({1^{st} (F)}^{-1} (x) 2^{nd} (F) {1^{st} (F)}^{-1} (y))}^{-1})$
144	141 139	eqeltrrd	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to ⟨1^{st} (F), 2^{nd} (F)⟩ \in ((X Full Y) \cap (X Faith Y))$
145	144 115	sylibr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to 1^{st} (F) ((X Full Y) \cap (X Faith Y)) 2^{nd} (F)$
146		simprr	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to 1^{st} (F) : R \underset{1-1 onto}{⟶} S$
147	1 2 3 4 142 134 135 10 143 145 146	catcisolem	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to ⟨1^{st} (F), 2^{nd} (F)⟩ (X Inv (C) Y) ⟨{1^{st} (F)}^{-1}, (x \in S, y \in S ⟼ {({1^{st} (F)}^{-1} (x) 2^{nd} (F) {1^{st} (F)}^{-1} (y))}^{-1})⟩$
148	141 147	eqbrtrd	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to F (X Inv (C) Y) ⟨{1^{st} (F)}^{-1}, (x \in S, y \in S ⟼ {({1^{st} (F)}^{-1} (x) 2^{nd} (F) {1^{st} (F)}^{-1} (y))}^{-1})⟩$
149	2 10 133 134 135 8 148	inviso1	$⊢ (φ \land (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S)) \to F \in (X I Y)$
150	132 149	impbida	$⊢ φ \to (F \in (X I Y) \leftrightarrow (F \in ((X Full Y) \cap (X Faith Y)) \land 1^{st} (F) : R \underset{1-1 onto}{⟶} S))$

Metamath Proof Explorer

Theorem catciso

Proof