Metamath Proof Explorer

Theorem funcsetcestrclem7

Description: Lemma 7 for funcsetcestrc . (Contributed by AV, 27-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 funcsetcestrclem7 
|- ( ( ph /\ X e. C ) -> ( ( X G X ) ` ( ( Id ` S ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )

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 funcsetcestrclem5 
 |-  ( ( ph /\ ( X e. C /\ X e. C ) ) -> ( X G X ) = ( _I |` ( X ^m X ) ) )
9 8 anabsan2 
 |-  ( ( ph /\ X e. C ) -> ( X G X ) = ( _I |` ( X ^m X ) ) )
10 eqid 
 |-  ( Id ` S ) = ( Id ` S )
11 4 adantr 
 |-  ( ( ph /\ X e. C ) -> U e. WUni )
12 1 4 setcbas 
 |-  ( ph -> U = ( Base ` S ) )
13 2 12 eqtr4id 
 |-  ( ph -> C = U )
14 13 eleq2d 
 |-  ( ph -> ( X e. C <-> X e. U ) )
15 14 biimpa 
 |-  ( ( ph /\ X e. C ) -> X e. U )
16 1 10 11 15 setcid 
 |-  ( ( ph /\ X e. C ) -> ( ( Id ` S ) ` X ) = ( _I |` X ) )
17 9 16 fveq12d 
 |-  ( ( ph /\ X e. C ) -> ( ( X G X ) ` ( ( Id ` S ) ` X ) ) = ( ( _I |` ( X ^m X ) ) ` ( _I |` X ) ) )
18 f1oi 
 |-  ( _I |` X ) : X -1-1-onto-> X
19 f1of 
 |-  ( ( _I |` X ) : X -1-1-onto-> X -> ( _I |` X ) : X --> X )
20 18 19 ax-mp 
 |-  ( _I |` X ) : X --> X
21 simpr 
 |-  ( ( ph /\ X e. C ) -> X e. C )
22 21 21 elmapd 
 |-  ( ( ph /\ X e. C ) -> ( ( _I |` X ) e. ( X ^m X ) <-> ( _I |` X ) : X --> X ) )
23 20 22 mpbiri 
 |-  ( ( ph /\ X e. C ) -> ( _I |` X ) e. ( X ^m X ) )
24 fvresi 
 |-  ( ( _I |` X ) e. ( X ^m X ) -> ( ( _I |` ( X ^m X ) ) ` ( _I |` X ) ) = ( _I |` X ) )
25 23 24 syl 
 |-  ( ( ph /\ X e. C ) -> ( ( _I |` ( X ^m X ) ) ` ( _I |` X ) ) = ( _I |` X ) )
26 eqid 
 |-  { <. ( Base ` ndx ) , X >. } = { <. ( Base ` ndx ) , X >. }
27 26 1strbas 
 |-  ( X e. C -> X = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
28 21 27 syl 
 |-  ( ( ph /\ X e. C ) -> X = ( Base ` { <. ( Base ` ndx ) , X >. } ) )
29 28 reseq2d 
 |-  ( ( ph /\ X e. C ) -> ( _I |` X ) = ( _I |` ( Base ` { <. ( Base ` ndx ) , X >. } ) ) )
30 25 29 eqtrd 
 |-  ( ( ph /\ X e. C ) -> ( ( _I |` ( X ^m X ) ) ` ( _I |` X ) ) = ( _I |` ( Base ` { <. ( Base ` ndx ) , X >. } ) ) )
31 1 2 3 funcsetcestrclem1 
 |-  ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )
32 31 fveq2d 
 |-  ( ( ph /\ X e. C ) -> ( ( Id ` E ) ` ( F ` X ) ) = ( ( Id ` E ) ` { <. ( Base ` ndx ) , X >. } ) )
33 eqid 
 |-  ( Id ` E ) = ( Id ` E )
34 1 2 4 5 setc1strwun 
 |-  ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. U )
35 7 33 11 34 estrcid 
 |-  ( ( ph /\ X e. C ) -> ( ( Id ` E ) ` { <. ( Base ` ndx ) , X >. } ) = ( _I |` ( Base ` { <. ( Base ` ndx ) , X >. } ) ) )
36 32 35 eqtr2d 
 |-  ( ( ph /\ X e. C ) -> ( _I |` ( Base ` { <. ( Base ` ndx ) , X >. } ) ) = ( ( Id ` E ) ` ( F ` X ) ) )
37 17 30 36 3eqtrd 
 |-  ( ( ph /\ X e. C ) -> ( ( X G X ) ` ( ( Id ` S ) ` X ) ) = ( ( Id ` E ) ` ( F ` X ) ) )