Theorem funcsetcestrclem3

Description: Lemma 3 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 )
	funcsetcestrclem3.e	|- E = ( ExtStrCat ` U )
	funcsetcestrclem3.b	|- B = ( Base ` E )
Assertion	funcsetcestrclem3	|- ( ph -> F : C --> B )

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		funcsetcestrclem3.e	|- E = ( ExtStrCat ` U )
7		funcsetcestrclem3.b	|- B = ( Base ` E )
8	1 2 4 5	setc1strwun	|- ( ( ph /\ x e. C ) -> { <. ( Base ` ndx ) , x >. } e. U )
9	6 4	estrcbas	|- ( ph -> U = ( Base ` E ) )
10	9	eqcomd	|- ( ph -> ( Base ` E ) = U )
11	10	adantr	|- ( ( ph /\ x e. C ) -> ( Base ` E ) = U )
12	8 11	eleqtrrd	|- ( ( ph /\ x e. C ) -> { <. ( Base ` ndx ) , x >. } e. ( Base ` E ) )
13	12 7	eleqtrrdi	|- ( ( ph /\ x e. C ) -> { <. ( Base ` ndx ) , x >. } e. B )
14	3 13	fmpt3d	|- ( ph -> F : C --> B )