Metamath Proof Explorer

Theorem fullestrcsetc

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 full. (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 fullestrcsetc 
|- ( ph -> F ( E Full 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 ` S ) = ( Hom ` S )
12 1 2 3 4 5 6 funcestrcsetclem2 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) e. U )
13 12 adantrr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) e. U )
14 1 2 3 4 5 6 funcestrcsetclem2 
 |-  ( ( ph /\ b e. B ) -> ( F ` b ) e. U )
15 14 adantrl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) e. U )
16 2 10 11 13 15 elsetchom 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h e. ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) <-> h : ( F ` a ) --> ( F ` b ) ) )
17 1 2 3 4 5 6 funcestrcsetclem1 
 |-  ( ( ph /\ a e. B ) -> ( F ` a ) = ( Base ` a ) )
18 17 adantrr 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` a ) = ( Base ` a ) )
19 1 2 3 4 5 6 funcestrcsetclem1 
 |-  ( ( ph /\ b e. B ) -> ( F ` b ) = ( Base ` b ) )
20 19 adantrl 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( F ` b ) = ( Base ` b ) )
21 18 20 feq23d 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h : ( F ` a ) --> ( F ` b ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
22 16 21 bitrd 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h e. ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
23 fvex 
 |-  ( Base ` b ) e. _V
24 fvex 
 |-  ( Base ` a ) e. _V
25 23 24 pm3.2i 
 |-  ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V )
26 elmapg 
 |-  ( ( ( Base ` b ) e. _V /\ ( Base ` a ) e. _V ) -> ( h e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
27 25 26 mp1i 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h e. ( ( Base ` b ) ^m ( Base ` a ) ) <-> h : ( Base ` a ) --> ( Base ` b ) ) )
28 27 biimpar 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> h e. ( ( Base ` b ) ^m ( Base ` a ) ) )
29 equequ2 
 |-  ( k = h -> ( h = k <-> h = h ) )
30 29 adantl 
 |-  ( ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) /\ k = h ) -> ( h = k <-> h = h ) )
31 eqidd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> h = h )
32 28 30 31 rspcedvd 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = k )
33 eqid 
 |-  ( Base ` a ) = ( Base ` a )
34 eqid 
 |-  ( Base ` b ) = ( Base ` b )
35 1 2 3 4 5 6 7 33 34 funcestrcsetclem6 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) /\ k e. ( ( Base ` b ) ^m ( Base ` a ) ) ) -> ( ( a G b ) ` k ) = k )
36 35 3expa 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ k e. ( ( Base ` b ) ^m ( Base ` a ) ) ) -> ( ( a G b ) ` k ) = k )
37 36 eqeq2d 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ k e. ( ( Base ` b ) ^m ( Base ` a ) ) ) -> ( h = ( ( a G b ) ` k ) <-> h = k ) )
38 37 rexbidva 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = ( ( a G b ) ` k ) <-> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = k ) )
39 38 adantr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> ( E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = ( ( a G b ) ` k ) <-> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = k ) )
40 32 39 mpbird 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = ( ( a G b ) ` k ) )
41 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
42 1 5 estrcbas 
 |-  ( ph -> U = ( Base ` E ) )
43 3 42 eqtr4id 
 |-  ( ph -> B = U )
44 43 eleq2d 
 |-  ( ph -> ( a e. B <-> a e. U ) )
45 44 biimpcd 
 |-  ( a e. B -> ( ph -> a e. U ) )
46 45 adantr 
 |-  ( ( a e. B /\ b e. B ) -> ( ph -> a e. U ) )
47 46 impcom 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> a e. U )
48 43 eleq2d 
 |-  ( ph -> ( b e. B <-> b e. U ) )
49 48 biimpcd 
 |-  ( b e. B -> ( ph -> b e. U ) )
50 49 adantl 
 |-  ( ( a e. B /\ b e. B ) -> ( ph -> b e. U ) )
51 50 impcom 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> b e. U )
52 1 10 41 47 51 33 34 estrchom 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a ( Hom ` E ) b ) = ( ( Base ` b ) ^m ( Base ` a ) ) )
53 52 rexeqdv 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) <-> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = ( ( a G b ) ` k ) ) )
54 53 adantr 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> ( E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) <-> E. k e. ( ( Base ` b ) ^m ( Base ` a ) ) h = ( ( a G b ) ` k ) ) )
55 40 54 mpbird 
 |-  ( ( ( ph /\ ( a e. B /\ b e. B ) ) /\ h : ( Base ` a ) --> ( Base ` b ) ) -> E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) )
56 55 ex 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h : ( Base ` a ) --> ( Base ` b ) -> E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) ) )
57 22 56 sylbid 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( h e. ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) -> E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) ) )
58 57 ralrimiv 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> A. h e. ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) )
59 dffo3 
 |-  ( ( a G b ) : ( a ( Hom ` E ) b ) -onto-> ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) <-> ( ( a G b ) : ( a ( Hom ` E ) b ) --> ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) /\ A. h e. ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) E. k e. ( a ( Hom ` E ) b ) h = ( ( a G b ) ` k ) ) )
60 9 58 59 sylanbrc 
 |-  ( ( ph /\ ( a e. B /\ b e. B ) ) -> ( a G b ) : ( a ( Hom ` E ) b ) -onto-> ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) )
61 60 ralrimivva 
 |-  ( ph -> A. a e. B A. b e. B ( a G b ) : ( a ( Hom ` E ) b ) -onto-> ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) )
62 3 11 41 isfull2 
 |-  ( F ( E Full S ) G <-> ( F ( E Func S ) G /\ A. a e. B A. b e. B ( a G b ) : ( a ( Hom ` E ) b ) -onto-> ( ( F ` a ) ( Hom ` S ) ( F ` b ) ) ) )
63 8 61 62 sylanbrc 
 |-  ( ph -> F ( E Full S ) G )