Metamath Proof Explorer

Theorem funcsetcestrclem8

Description: Lemma 8 for funcsetcestrc . (Contributed by AV, 28-Mar-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 funcsetcestrclem8 
|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) : ( X ( Hom ` S ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )

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 f1oi 
 |-  ( _I |` ( Y ^m X ) ) : ( Y ^m X ) -1-1-onto-> ( Y ^m X )
9 f1of 
 |-  ( ( _I |` ( Y ^m X ) ) : ( Y ^m X ) -1-1-onto-> ( Y ^m X ) -> ( _I |` ( Y ^m X ) ) : ( Y ^m X ) --> ( Y ^m X ) )
10 8 9 mp1i 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( _I |` ( Y ^m X ) ) : ( Y ^m X ) --> ( Y ^m X ) )
11 elmapi 
 |-  ( f e. ( Y ^m X ) -> f : X --> Y )
12 simpr 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X e. C /\ Y e. C ) )
13 12 ancomd 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Y e. C /\ X e. C ) )
14 elmapg 
 |-  ( ( Y e. C /\ X e. C ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) )
15 13 14 syl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( f e. ( Y ^m X ) <-> f : X --> Y ) )
16 15 biimpar 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C ) ) /\ f : X --> Y ) -> f e. ( Y ^m X ) )
17 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ Y e. C ) -> ( F ` Y ) = { <. ( Base ` ndx ) , Y >. } )
18 17 fveq2d 
 |-  ( ( ph /\ Y e. C ) -> ( Base ` ( F ` Y ) ) = ( Base ` { <. ( Base ` ndx ) , Y >. } ) )
19 eqid 
 |-  { <. ( Base ` ndx ) , Y >. } = { <. ( Base ` ndx ) , Y >. }
20 19 1strbas 
 |-  ( Y e. C -> Y = ( Base ` { <. ( Base ` ndx ) , Y >. } ) )
21 20 eqcomd 
 |-  ( Y e. C -> ( Base ` { <. ( Base ` ndx ) , Y >. } ) = Y )
22 21 adantl 
 |-  ( ( ph /\ Y e. C ) -> ( Base ` { <. ( Base ` ndx ) , Y >. } ) = Y )
23 18 22 eqtrd 
 |-  ( ( ph /\ Y e. C ) -> ( Base ` ( F ` Y ) ) = Y )
24 23 adantrl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Base ` ( F ` Y ) ) = Y )
25 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )
26 25 fveq2d 
 |-  ( ( ph /\ X e. C ) -> ( Base ` ( F ` X ) ) = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
27 eqid 
 |-  { <. ( Base ` ndx ) , X >. } = { <. ( Base ` ndx ) , X >. }
28 27 1strbas 
 |-  ( X e. C -> X = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
29 28 adantl 
 |-  ( ( ph /\ X e. C ) -> X = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
30 26 29 eqtr4d 
 |-  ( ( ph /\ X e. C ) -> ( Base ` ( F ` X ) ) = X )
31 30 adantrr 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Base ` ( F ` X ) ) = X )
32 24 31 oveq12d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) = ( Y ^m X ) )
33 32 adantr 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C ) ) /\ f : X --> Y ) -> ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) = ( Y ^m X ) )
34 16 33 eleqtrrd 
 |-  ( ( ( ph /\ ( X e. C /\ Y e. C ) ) /\ f : X --> Y ) -> f e. ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) )
35 34 ex 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( f : X --> Y -> f e. ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) ) )
36 11 35 syl5 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( f e. ( Y ^m X ) -> f e. ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) ) )
37 36 ssrdv 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Y ^m X ) C_ ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) )
38 10 37 fssd 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( _I |` ( Y ^m X ) ) : ( Y ^m X ) --> ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) )
39 1 2 3 4 5 6 funcsetcestrclem5 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) )
40 4 adantr 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> U e. WUni )
41 eqid 
 |-  ( Hom ` S ) = ( Hom ` S )
42 1 4 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
43 2 42 eqtr4id 
 |-  ( ph -> C = U )
44 43 eleq2d 
 |-  ( ph -> ( X e. C <-> X e. U ) )
45 44 biimpd 
 |-  ( ph -> ( X e. C -> X e. U ) )
46 45 adantrd 
 |-  ( ph -> ( ( X e. C /\ Y e. C ) -> X e. U ) )
47 46 imp 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> X e. U )
48 43 eleq2d 
 |-  ( ph -> ( Y e. C <-> Y e. U ) )
49 48 biimpd 
 |-  ( ph -> ( Y e. C -> Y e. U ) )
50 49 adantld 
 |-  ( ph -> ( ( X e. C /\ Y e. C ) -> Y e. U ) )
51 50 imp 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> Y e. U )
52 1 40 41 47 51 setchom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X ( Hom ` S ) Y ) = ( Y ^m X ) )
53 eqid 
 |-  ( Hom ` E ) = ( Hom ` E )
54 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) e. U )
55 54 adantrr 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( F ` X ) e. U )
56 1 2 3 4 5 funcsetcestrclem2 
 |-  ( ( ph /\ Y e. C ) -> ( F ` Y ) e. U )
57 56 adantrl 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( F ` Y ) e. U )
58 eqid 
 |-  ( Base ` ( F ` X ) ) = ( Base ` ( F ` X ) )
59 eqid 
 |-  ( Base ` ( F ` Y ) ) = ( Base ` ( F ` Y ) )
60 7 40 53 55 57 58 59 estrchom 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) = ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) )
61 39 52 60 feq123d 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( ( X G Y ) : ( X ( Hom ` S ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) <-> ( _I |` ( Y ^m X ) ) : ( Y ^m X ) --> ( ( Base ` ( F ` Y ) ) ^m ( Base ` ( F ` X ) ) ) ) )
62 38 61 mpbird 
 |-  ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) : ( X ( Hom ` S ) Y ) --> ( ( F ` X ) ( Hom ` E ) ( F ` Y ) ) )