This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )