Metamath Proof Explorer

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