Metamath Proof Explorer


Theorem funcsetcestrclem2

Description: Lemma 2 for funcsetcestrc . (Contributed by AV, 27-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s S=SetCatU
funcsetcestrc.c C=BaseS
funcsetcestrc.f φF=xCBasendxx
funcsetcestrc.u φUWUni
funcsetcestrc.o φωU
Assertion funcsetcestrclem2 φXCFXU

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s S=SetCatU
2 funcsetcestrc.c C=BaseS
3 funcsetcestrc.f φF=xCBasendxx
4 funcsetcestrc.u φUWUni
5 funcsetcestrc.o φωU
6 1 2 3 funcsetcestrclem1 φXCFX=BasendxX
7 1 2 4 5 setc1strwun φXCBasendxXU
8 6 7 eqeltrd φXCFXU