Metamath Proof Explorer

Theorem fthsetcestrc

Description: The "embedding functor" from the category of sets into the category of extensible structures which sends each set to an extensible structure consisting of the base set slot only is faithful. (Contributed by AV, 31-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s 
|- S = ( SetCat ` U )
funcsetcestrc.c 
|- C = ( Base ` S )
funcsetcestrc.f 
|- ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
funcsetcestrc.u 
|- ( ph -> U e. WUni )
funcsetcestrc.o 
|- ( ph -> _om e. U )
funcsetcestrc.g 
|- ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )
funcsetcestrc.e 
|- E = ( ExtStrCat ` U )
Assertion fthsetcestrc 
|- ( ph -> F ( S Faith E ) G )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s 
 |-  S = ( SetCat ` U )
2 funcsetcestrc.c 
 |-  C = ( Base ` S )
3 funcsetcestrc.f 
 |-  ( ph -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
4 funcsetcestrc.u 
 |-  ( ph -> U e. WUni )
5 funcsetcestrc.o 
 |-  ( ph -> _om e. U )
6 funcsetcestrc.g 
 |-  ( ph -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )
7 funcsetcestrc.e 
 |-  E = ( ExtStrCat ` U )
8 1 2 3 4 5 6 7 funcsetcestrc 
 |-  ( ph -> F ( S Func E ) G )
9 1 2 3 4 5 6 7 funcsetcestrclem8 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a G b ) : ( a ( Hom ` S ) b ) --> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) )
10 4 adantr 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> U e. WUni )
11 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
12 1 4 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
13 2 12 eqtr4id 
 |-  ( ph -> C = U )
14 13 eleq2d 
 |-  ( ph -> ( a e. C <-> a e. U ) )
15 14 biimpcd 
 |-  ( a e. C -> ( ph -> a e. U ) )
16 15 adantr 
 |-  ( ( a e. C /\ b e. C ) -> ( ph -> a e. U ) )
17 16 impcom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> a e. U )
18 13 eleq2d 
 |-  ( ph -> ( b e. C <-> b e. U ) )
19 18 biimpcd 
 |-  ( b e. C -> ( ph -> b e. U ) )
20 19 adantl 
 |-  ( ( a e. C /\ b e. C ) -> ( ph -> b e. U ) )
21 20 impcom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> b e. U )
22 1 10 11 17 21 setchom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a ( Hom ` S ) b ) = ( b ^m a ) )
23 22 eleq2d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( a ( Hom ` S ) b ) <-> h e. ( b ^m a ) ) )
24 1 2 3 4 5 6 funcsetcestrclem6 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) /\ h e. ( b ^m a ) ) -> ( ( a G b ) ` h ) = h )
25 24 3expia 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( b ^m a ) -> ( ( a G b ) ` h ) = h ) )
26 23 25 sylbid 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( a ( Hom ` S ) b ) -> ( ( a G b ) ` h ) = h ) )
27 26 com12 
 |-  ( h e. ( a ( Hom ` S ) b ) -> ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( ( a G b ) ` h ) = h ) )
28 27 adantr 
 |-  ( ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) -> ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( ( a G b ) ` h ) = h ) )
29 28 impcom 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) ) -> ( ( a G b ) ` h ) = h )
30 22 eleq2d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( k e. ( a ( Hom ` S ) b ) <-> k e. ( b ^m a ) ) )
31 1 2 3 4 5 6 funcsetcestrclem6 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) /\ k e. ( b ^m a ) ) -> ( ( a G b ) ` k ) = k )
32 31 3expia 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( k e. ( b ^m a ) -> ( ( a G b ) ` k ) = k ) )
33 30 32 sylbid 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( k e. ( a ( Hom ` S ) b ) -> ( ( a G b ) ` k ) = k ) )
34 33 com12 
 |-  ( k e. ( a ( Hom ` S ) b ) -> ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( ( a G b ) ` k ) = k ) )
35 34 adantl 
 |-  ( ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) -> ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( ( a G b ) ` k ) = k ) )
36 35 impcom 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) ) -> ( ( a G b ) ` k ) = k )
37 29 36 eqeq12d 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) ) -> ( ( ( a G b ) ` h ) = ( ( a G b ) ` k ) <-> h = k ) )
38 37 biimpd 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ ( h e. ( a ( Hom ` S ) b ) /\ k e. ( a ( Hom ` S ) b ) ) ) -> ( ( ( a G b ) ` h ) = ( ( a G b ) ` k ) -> h = k ) )
39 38 ralrimivva 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> A. h e. ( a ( Hom ` S ) b ) A. k e. ( a ( Hom ` S ) b ) ( ( ( a G b ) ` h ) = ( ( a G b ) ` k ) -> h = k ) )
40 dff13 
 |-  ( ( a G b ) : ( a ( Hom ` S ) b ) -1-1-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) <-> ( ( a G b ) : ( a ( Hom ` S ) b ) --> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) /\ A. h e. ( a ( Hom ` S ) b ) A. k e. ( a ( Hom ` S ) b ) ( ( ( a G b ) ` h ) = ( ( a G b ) ` k ) -> h = k ) ) )
41 9 39 40 sylanbrc 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a G b ) : ( a ( Hom ` S ) b ) -1-1-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) )
42 41 ralrimivva 
 |-  ( ph -> A. a e. C A. b e. C ( a G b ) : ( a ( Hom ` S ) b ) -1-1-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) )
43 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
44 2 11 43 isfth2 
 |-  ( F ( S Faith E ) G <-> ( F ( S Func E ) G /\ A. a e. C A. b e. C ( a G b ) : ( a ( Hom ` S ) b ) -1-1-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) ) )
45 8 42 44 sylanbrc 
 |-  ( ph -> F ( S Faith E ) G )