Metamath Proof Explorer

Theorem fthestrcsetc

Description: The "natural forgetful functor" from the category of extensible structures into the category of sets which sends each extensible structure to its base set is faithful. (Contributed by AV, 2-Apr-2020)

Ref Expression
Hypotheses funcestrcsetc.e 
|- E = ( ExtStrCat ` U )
funcestrcsetc.s 
|- S = ( SetCat ` U )
funcestrcsetc.b 
|- B = ( Base ` E )
funcestrcsetc.c 
|- C = ( Base ` S )
funcestrcsetc.u 
|- ( ph -> U e. WUni )
funcestrcsetc.f 
|- ( ph -> F = ( x e. B |-> ( Base ` x ) ) )
funcestrcsetc.g 
|- ( ph -> G = ( x e. B , y e. B |-> ( _I |` ( ( Base ` y ) ^m ( Base ` x ) ) ) ) )
Assertion fthestrcsetc 
|- ( ph -> F ( E Faith S ) G )

Proof

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