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	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	catciso.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
	catciso.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
	catciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	catciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	catciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	catciso.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
Assertion	catciso	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		catciso.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catciso.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		catciso.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
4		catciso.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
5		catciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		catciso.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7		catciso.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8		catciso.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
9		relfunc	⊢ Rel ( 𝑋 Func 𝑌 )
10		eqid	⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
11	1	catccat	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
12	5 11	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	2 10 12 6 7 8	isoval	⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
14	13	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ) )
15	14	biimpa	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
16	12	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐶 ∈ Cat )
17	6	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ 𝐵 )
18	7	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ 𝐵 )
19	2 10 16 17 18	invfun	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
20		funfvbrb	⊢ ( Fun ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
21	19 20	syl	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ∈ dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ↔ 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
22	15 21	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) )
23		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
24	2 10 16 17 18 23	isinv	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
25	22 24	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
26	25	simpld	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) )
27		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
28		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
29		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
30	2 27 28 29 23 16 17 18	issect	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ) )
31	26 30	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
32	31	simp1d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
33	1 2 5 27 6 7	catchom	⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( 𝑋 Func 𝑌 ) )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( 𝑋 Func 𝑌 ) )
35	32 34	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
36		1st2nd	⊢ ( ( Rel ( 𝑋 Func 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 Func 𝑌 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
37	9 35 36	sylancr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
38		1st2ndbr	⊢ ( ( Rel ( 𝑋 Func 𝑌 ) ∧ 𝐹 ∈ ( 𝑋 Func 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) )
39	9 35 38	sylancr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) )
40		eqid	⊢ ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
41		eqid	⊢ ( Hom ‘ 𝑌 ) = ( Hom ‘ 𝑌 )
42	39	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) )
43		simprl	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
44		simprr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
45	3 40 41 42 43 44	funcf2	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
46		relfunc	⊢ Rel ( 𝑌 Func 𝑋 )
47	31	simp2d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
48	1 2 5 27 7 6	catchom	⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑌 Func 𝑋 ) )
49	48	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑌 Func 𝑋 ) )
50	47 49	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 Func 𝑋 ) )
51		1st2ndbr	⊢ ( ( Rel ( 𝑌 Func 𝑋 ) ∧ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 Func 𝑋 ) ) → ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( 𝑌 Func 𝑋 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
52	46 50 51	sylancr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( 𝑌 Func 𝑋 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
53	52	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( 𝑌 Func 𝑋 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
54	3 4 42	funcf1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1^st ‘ 𝐹 ) : 𝑅 ⟶ 𝑆 )
55	54 43	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑆 )
56	54 44	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ 𝑆 )
57	4 41 40 53 55 56	funcf2	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝑋 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
58	31	simp3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
59	5	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑈 ∈ 𝑉 )
60	1 2 59 28 17 18 17 35 50	catcco	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝐹 ) = ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) )
61		eqid	⊢ ( id_func ‘ 𝑋 ) = ( id_func ‘ 𝑋 )
62	1 2 29 61 5 6	catcid	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( id_func ‘ 𝑋 ) )
63	62	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( id_func ‘ 𝑋 ) )
64	58 60 63	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) = ( id_func ‘ 𝑋 ) )
65	64	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) = ( id_func ‘ 𝑋 ) )
66	65	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) = ( 1^st ‘ ( id_func ‘ 𝑋 ) ) )
67	66	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( id_func ‘ 𝑋 ) ) ‘ 𝑥 ) )
68	35	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
69	50	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 Func 𝑋 ) )
70	3 68 69 43	cofu1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
71	1 2 5	catcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
72		inss2	⊢ ( 𝑈 ∩ Cat ) ⊆ Cat
73	71 72	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ Cat )
74	73 6	sseldd	⊢ ( 𝜑 → 𝑋 ∈ Cat )
75	74	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑋 ∈ Cat )
76	61 3 75 43	idfu1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( id_func ‘ 𝑋 ) ) ‘ 𝑥 ) = 𝑥 )
77	67 70 76	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = 𝑥 )
78	66	fveq1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( id_func ‘ 𝑋 ) ) ‘ 𝑦 ) )
79	3 68 69 44	cofu1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
80	61 3 75 44	idfu1	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( id_func ‘ 𝑋 ) ) ‘ 𝑦 ) = 𝑦 )
81	78 79 80	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = 𝑦 )
82	77 81	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝑋 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) )
83	82	feq3d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝑋 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ↔ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ) )
84	57 83	mpbid	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ⟶ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) )
85	65	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 2^nd ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) = ( 2^nd ‘ ( id_func ‘ 𝑋 ) ) )
86	85	oveqd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) 𝑦 ) = ( 𝑥 ( 2^nd ‘ ( id_func ‘ 𝑋 ) ) 𝑦 ) )
87	3 68 69 43 44	cofu2nd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) 𝑦 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
88	61 3 75 40 43 44	idfu2nd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ ( id_func ‘ 𝑋 ) ) 𝑦 ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ) )
89	86 87 88	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) = ( I ↾ ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) ) )
90	25	simprd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
91	2 27 28 29 23 16 18 17	issect	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ↔ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) ) )
92	90 91	mpbid	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝐹 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) ∧ ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
93	92	simp3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
94	1 2 59 28 18 17 18 50 35	catcco	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) )
95		eqid	⊢ ( id_func ‘ 𝑌 ) = ( id_func ‘ 𝑌 )
96	1 2 29 95 5 7	catcid	⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) = ( id_func ‘ 𝑌 ) )
97	96	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) = ( id_func ‘ 𝑌 ) )
98	93 94 97	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( id_func ‘ 𝑌 ) )
99	98	adantr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) = ( id_func ‘ 𝑌 ) )
100	99	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 2^nd ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) = ( 2^nd ‘ ( id_func ‘ 𝑌 ) ) )
101	100	oveqd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( id_func ‘ 𝑌 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
102	4 69 68 55 56	cofu2nd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ∘ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
103	77 81	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
104	103	coeq1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( 2^nd ‘ 𝐹 ) ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ∘ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
105	102 104	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
106	73	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝐵 ⊆ Cat )
107	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑌 ∈ 𝐵 )
108	106 107	sseldd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑌 ∈ Cat )
109	95 4 108 41 55 56	idfu2nd	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( id_func ‘ 𝑌 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) = ( I ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
110	101 105 109	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ∘ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( I ↾ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
111	45 84 89 110	fcof1od	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
112	111	ralrimivva	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
113	3 40 41	isffth2	⊢ ( ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) ↔ ( ( 1^st ‘ 𝐹 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝑋 ) 𝑦 ) –1-1-onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝑌 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
114	39 112 113	sylanbrc	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) )
115		df-br	⊢ ( ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) ↔ ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
116	114 115	sylib	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
117	37 116	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
118	3 4 39	funcf1	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ 𝐹 ) : 𝑅 ⟶ 𝑆 )
119	4 3 52	funcf1	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) : 𝑆 ⟶ 𝑅 )
120	64	fveq2d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) = ( 1^st ‘ ( id_func ‘ 𝑋 ) ) )
121	3 35 50	cofu1st	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∘_func 𝐹 ) ) = ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ∘ ( 1^st ‘ 𝐹 ) ) )
122	74	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑋 ∈ Cat )
123	61 3 122	idfu1st	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( id_func ‘ 𝑋 ) ) = ( I ↾ 𝑅 ) )
124	120 121 123	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ∘ ( 1^st ‘ 𝐹 ) ) = ( I ↾ 𝑅 ) )
125	98	fveq2d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) = ( 1^st ‘ ( id_func ‘ 𝑌 ) ) )
126	4 50 35	cofu1st	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( 𝐹 ∘_func ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) = ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) )
127	73 7	sseldd	⊢ ( 𝜑 → 𝑌 ∈ Cat )
128	127	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → 𝑌 ∈ Cat )
129	95 4 128	idfu1st	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ ( id_func ‘ 𝑌 ) ) = ( I ↾ 𝑆 ) )
130	125 126 129	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( ( 1^st ‘ 𝐹 ) ∘ ( 1^st ‘ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ) ) = ( I ↾ 𝑆 ) )
131	118 119 124 130	fcof1od	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 )
132	117 131	jca	⊢ ( ( 𝜑 ∧ 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ) → ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) )
133	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐶 ∈ Cat )
134	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑋 ∈ 𝐵 )
135	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑌 ∈ 𝐵 )
136		inss1	⊢ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ⊆ ( 𝑋 Full 𝑌 )
137		fullfunc	⊢ ( 𝑋 Full 𝑌 ) ⊆ ( 𝑋 Func 𝑌 )
138	136 137	sstri	⊢ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ⊆ ( 𝑋 Func 𝑌 )
139		simprl	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
140	138 139	sseldi	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐹 ∈ ( 𝑋 Func 𝑌 ) )
141	9 140 36	sylancr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
142	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑈 ∈ 𝑉 )
143		eqid	⊢ ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ^◡ ( ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ^◡ ( ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
144	141 139	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
145	144 115	sylibr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 1^st ‘ 𝐹 ) ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ( 2^nd ‘ 𝐹 ) )
146		simprr	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 )
147	1 2 3 4 142 134 135 10 143 145 146	catcisolem	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⟨ ^◡ ( 1^st ‘ 𝐹 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ^◡ ( ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ⟩ )
148	141 147	eqbrtrd	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐹 ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⟨ ^◡ ( 1^st ‘ 𝐹 ) , ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ^◡ ( ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐹 ) ( ^◡ ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ⟩ )
149	2 10 133 134 135 8 148	inviso1	⊢ ( ( 𝜑 ∧ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
150	132 149	impbida	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )

Metamath Proof Explorer

Theorem catciso

Proof