This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcestrcsetc

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, preserving the morphisms as mappings between the corresponding base sets. (Contributed by AV, 23-Mar-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 funcestrcsetc 
|- ( ph -> F ( E Func 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 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
9 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
10 eqid 
 |-  ( Id ` E ) = ( Id ` E )
11 eqid 
 |-  ( Id ` S ) = ( Id ` S )
12 eqid 
 |-  ( comp ` E ) = ( comp ` E )
13 eqid 
 |-  ( comp ` S ) = ( comp ` S )
14 1 estrccat 
 |-  ( U e. WUni -> E e. Cat )
15 5 14 syl 
 |-  ( ph -> E e. Cat )
16 2 setccat 
 |-  ( U e. WUni -> S e. Cat )
17 5 16 syl 
 |-  ( ph -> S e. Cat )
18 1 2 3 4 5 6 funcestrcsetclem3 
 |-  ( ph -> F : B --> C )
19 1 2 3 4 5 6 7 funcestrcsetclem4 
 |-  ( ph -> G Fn ( B X. B ) )
20 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 ) ) )
21 1 2 3 4 5 6 7 funcestrcsetclem7 
 |-  ( ( ph /\ a e. B ) -> ( ( a G a ) ` ( ( Id ` E ) ` a ) ) = ( ( Id ` S ) ` ( F ` a ) ) )
22 1 2 3 4 5 6 7 funcestrcsetclem9 
 |-  ( ( ph /\ ( a e. B /\ b e. B /\ c e. B ) /\ ( h e. ( a ( Hom ` E ) b ) /\ k e. ( b ( Hom ` E ) c ) ) ) -> ( ( a G c ) ` ( k ( <. a , b >. ( comp ` E ) c ) h ) ) = ( ( ( b G c ) ` k ) ( <. ( F ` a ) , ( F ` b ) >. ( comp ` S ) ( F ` c ) ) ( ( a G b ) ` h ) ) )
23 3 4 8 9 10 11 12 13 15 17 18 19 20 21 22 isfuncd 
 |-  ( ph -> F ( E Func S ) G )