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 )