Theorem funcsetcestrclem1

Description: Lemma 1 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 >. } ) )
Assertion	funcsetcestrclem1	|- ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , 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	3	adantr	|- ( ( ph /\ X e. C ) -> F = ( x e. C |-> { <. ( Base ` ndx ) , x >. } ) )
5		opeq2	|- ( x = X -> <. ( Base ` ndx ) , x >. = <. ( Base ` ndx ) , X >. )
6	5	sneqd	|- ( x = X -> { <. ( Base ` ndx ) , x >. } = { <. ( Base ` ndx ) , X >. } )
7	6	adantl	|- ( ( ( ph /\ X e. C ) /\ x = X ) -> { <. ( Base ` ndx ) , x >. } = { <. ( Base ` ndx ) , X >. } )
8		simpr	|- ( ( ph /\ X e. C ) -> X e. C )
9		snex	|- { <. ( Base ` ndx ) , X >. } e. _V
10	9	a1i	|- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. _V )
11	4 7 8 10	fvmptd	|- ( ( ph /\ X e. C ) -> ( F ` X ) = { <. ( Base ` ndx ) , X >. } )