Metamath Proof Explorer


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 )