Metamath Proof Explorer

Theorem fullsetcestrc

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 full. (Contributed by AV, 1-Apr-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 fullsetcestrc 
|- ( ph -> F ( S Full 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 ` E ) = ( Hom ` E )
12 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ a e. C ) -> ( F ` a ) e. U )
13 12 adantrr 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( F ` a ) e. U )
14 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ b e. C ) -> ( F ` b ) e. U )
15 14 adantrl 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( F ` b ) e. U )
16 eqid 
 |-  ( Base ` ( F ` a ) ) = ( Base ` ( F ` a ) )
17 eqid 
 |-  ( Base ` ( F ` b ) ) = ( Base ` ( F ` b ) )
18 7 10 11 13 15 16 17 elestrchom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) <-> h : ( Base ` ( F ` a ) ) --> ( Base ` ( F ` b ) ) ) )
19 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ a e. C ) -> ( F ` a ) = { <. ( Base ` ndx ) , a >. } )
20 19 adantrr 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( F ` a ) = { <. ( Base ` ndx ) , a >. } )
21 20 fveq2d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( Base ` ( F ` a ) ) = ( Base ` { <. ( Base ` ndx ) , a >. } ) )
22 eqid 
 |-  { <. ( Base ` ndx ) , a >. } = { <. ( Base ` ndx ) , a >. }
23 22 1strbas 
 |-  ( a e. C -> a = ( Base ` { <. ( Base ` ndx ) , a >. } ) )
24 23 ad2antrl 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> a = ( Base ` { <. ( Base ` ndx ) , a >. } ) )
25 21 24 eqtr4d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( Base ` ( F ` a ) ) = a )
26 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ b e. C ) -> ( F ` b ) = { <. ( Base ` ndx ) , b >. } )
27 26 adantrl 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( F ` b ) = { <. ( Base ` ndx ) , b >. } )
28 27 fveq2d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( Base ` ( F ` b ) ) = ( Base ` { <. ( Base ` ndx ) , b >. } ) )
29 eqid 
 |-  { <. ( Base ` ndx ) , b >. } = { <. ( Base ` ndx ) , b >. }
30 29 1strbas 
 |-  ( b e. C -> b = ( Base ` { <. ( Base ` ndx ) , b >. } ) )
31 30 ad2antll 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> b = ( Base ` { <. ( Base ` ndx ) , b >. } ) )
32 28 31 eqtr4d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( Base ` ( F ` b ) ) = b )
33 25 32 feq23d 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h : ( Base ` ( F ` a ) ) --> ( Base ` ( F ` b ) ) <-> h : a --> b ) )
34 simpr 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a e. C /\ b e. C ) )
35 34 ancomd 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( b e. C /\ a e. C ) )
36 elmapg 
 |-  ( ( b e. C /\ a e. C ) -> ( h e. ( b ^m a ) <-> h : a --> b ) )
37 35 36 syl 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( b ^m a ) <-> h : a --> b ) )
38 37 biimpar 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> h e. ( b ^m a ) )
39 equequ2 
 |-  ( k = h -> ( h = k <-> h = h ) )
40 39 adantl 
 |-  ( ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) /\ k = h ) -> ( h = k <-> h = h ) )
41 eqidd 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> h = h )
42 38 40 41 rspcedvd 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> E. k e. ( b ^m a ) h = k )
43 1 2 3 4 5 6 funcsetcestrclem6 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) /\ k e. ( b ^m a ) ) -> ( ( a G b ) ` k ) = k )
44 43 3expa 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ k e. ( b ^m a ) ) -> ( ( a G b ) ` k ) = k )
45 44 eqeq2d 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ k e. ( b ^m a ) ) -> ( h = ( ( a G b ) ` k ) <-> h = k ) )
46 45 rexbidva 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( E. k e. ( b ^m a ) h = ( ( a G b ) ` k ) <-> E. k e. ( b ^m a ) h = k ) )
47 46 adantr 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> ( E. k e. ( b ^m a ) h = ( ( a G b ) ` k ) <-> E. k e. ( b ^m a ) h = k ) )
48 42 47 mpbird 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> E. k e. ( b ^m a ) h = ( ( a G b ) ` k ) )
49 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
50 1 4 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
51 2 50 eqtr4id 
 |-  ( ph -> C = U )
52 51 eleq2d 
 |-  ( ph -> ( a e. C <-> a e. U ) )
53 52 biimpcd 
 |-  ( a e. C -> ( ph -> a e. U ) )
54 53 adantr 
 |-  ( ( a e. C /\ b e. C ) -> ( ph -> a e. U ) )
55 54 impcom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> a e. U )
56 51 eleq2d 
 |-  ( ph -> ( b e. C <-> b e. U ) )
57 56 biimpcd 
 |-  ( b e. C -> ( ph -> b e. U ) )
58 57 adantl 
 |-  ( ( a e. C /\ b e. C ) -> ( ph -> b e. U ) )
59 58 impcom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> b e. U )
60 1 10 49 55 59 setchom 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a ( Hom ` S ) b ) = ( b ^m a ) )
61 60 rexeqdv 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) <-> E. k e. ( b ^m a ) h = ( ( a G b ) ` k ) ) )
62 61 adantr 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> ( E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) <-> E. k e. ( b ^m a ) h = ( ( a G b ) ` k ) ) )
63 48 62 mpbird 
 |-  ( ( ( ph /\ ( a e. C /\ b e. C ) ) /\ h : a --> b ) -> E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) )
64 63 ex 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h : a --> b -> E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) ) )
65 33 64 sylbid 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h : ( Base ` ( F ` a ) ) --> ( Base ` ( F ` b ) ) -> E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) ) )
66 18 65 sylbid 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( h e. ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) -> E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) ) )
67 66 ralrimiv 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> A. h e. ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) )
68 dffo3 
 |-  ( ( a G b ) : ( a ( Hom ` S ) b ) -onto-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) <-> ( ( a G b ) : ( a ( Hom ` S ) b ) --> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) /\ A. h e. ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) E. k e. ( a ( Hom ` S ) b ) h = ( ( a G b ) ` k ) ) )
69 9 67 68 sylanbrc 
 |-  ( ( ph /\ ( a e. C /\ b e. C ) ) -> ( a G b ) : ( a ( Hom ` S ) b ) -onto-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) )
70 69 ralrimivva 
 |-  ( ph -> A. a e. C A. b e. C ( a G b ) : ( a ( Hom ` S ) b ) -onto-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) )
71 2 11 49 isfull2 
 |-  ( F ( S Full E ) G <-> ( F ( S Func E ) G /\ A. a e. C A. b e. C ( a G b ) : ( a ( Hom ` S ) b ) -onto-> ( ( F ` a ) ( Hom ` E ) ( F ` b ) ) ) )
72 8 70 71 sylanbrc 
 |-  ( ph -> F ( S Full E ) G )