Theorem setc1strwun

Description: A constructed one-slot structure with the objects of the category of sets as base set in a weak universe. (Contributed by AV, 27-Mar-2020)

	Ref	Expression
Hypotheses	setc1strwun.s	|- S = ( SetCat ` U )
	setc1strwun.c	|- C = ( Base ` S )
	setc1strwun.u	|- ( ph -> U e. WUni )
	setc1strwun.o	|- ( ph -> _om e. U )
Assertion	setc1strwun	|- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. U )

Proof

Step	Hyp	Ref	Expression
1		setc1strwun.s	|- S = ( SetCat ` U )
2		setc1strwun.c	|- C = ( Base ` S )
3		setc1strwun.u	|- ( ph -> U e. WUni )
4		setc1strwun.o	|- ( ph -> _om e. U )
5	1 3	setcbas	|- ( ph -> U = ( Base ` S ) )
6	2 5	eqtr4id	|- ( ph -> C = U )
7	6	eleq2d	|- ( ph -> ( X e. C <-> X e. U ) )
8	7	biimpa	|- ( ( ph /\ X e. C ) -> X e. U )
9		eqid	|- { <. ( Base ` ndx ) , X >. } = { <. ( Base ` ndx ) , X >. }
10	9 3 4	1strwun	|- ( ( ph /\ X e. U ) -> { <. ( Base ` ndx ) , X >. } e. U )
11	8 10	syldan	|- ( ( ph /\ X e. C ) -> { <. ( Base ` ndx ) , X >. } e. U )