Theorem funcsetcestrclem5

Description: Lemma 5 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 ) ) ) )
Assertion	funcsetcestrclem5	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m 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	6	adantr	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> G = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) )
8		oveq12	|- ( ( y = Y /\ x = X ) -> ( y ^m x ) = ( Y ^m X ) )
9	8	ancoms	|- ( ( x = X /\ y = Y ) -> ( y ^m x ) = ( Y ^m X ) )
10	9	reseq2d	|- ( ( x = X /\ y = Y ) -> ( _I |` ( y ^m x ) ) = ( _I |` ( Y ^m X ) ) )
11	10	adantl	|- ( ( ( ph /\ ( X e. C /\ Y e. C ) ) /\ ( x = X /\ y = Y ) ) -> ( _I |` ( y ^m x ) ) = ( _I |` ( Y ^m X ) ) )
12		simprl	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> X e. C )
13		simprr	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> Y e. C )
14		ovexd	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( Y ^m X ) e. _V )
15	14	resiexd	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( _I |` ( Y ^m X ) ) e. _V )
16	7 11 12 13 15	ovmpod	|- ( ( ph /\ ( X e. C /\ Y e. C ) ) -> ( X G Y ) = ( _I |` ( Y ^m X ) ) )