Theorem funcsetcestrclem4

Description: Lemma 4 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	funcsetcestrclem4	|- ( ph -> G Fn ( C X. C ) )

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		eqid	|- ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) = ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) )
8		ovex	|- ( y ^m x ) e. _V
9		resiexg	|- ( ( y ^m x ) e. _V -> ( _I |` ( y ^m x ) ) e. _V )
10	8 9	ax-mp	|- ( _I |` ( y ^m x ) ) e. _V
11	7 10	fnmpoi	|- ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) Fn ( C X. C )
12	6	fneq1d	|- ( ph -> ( G Fn ( C X. C ) <-> ( x e. C , y e. C |-> ( _I |` ( y ^m x ) ) ) Fn ( C X. C ) ) )
13	11 12	mpbiri	|- ( ph -> G Fn ( C X. C ) )