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

Metamath Proof Explorer

Theorem wunex

Description: Construct a weak universe from a given set. See also wunex2 . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion wunex 
|- ( A e. V -> E. u e. WUni A C_ u )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) = ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om )
2 eqid 
 |-  U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) = U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om )
3 1 2 wunex2 
 |-  ( A e. V -> ( U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) e. WUni /\ A C_ U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) ) )
4 sseq2 
 |-  ( u = U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) -> ( A C_ u <-> A C_ U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) ) )
5 4 rspcev 
 |-  ( ( U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) e. WUni /\ A C_ U. ran ( rec ( ( z e. _V |-> ( ( z u. U. z ) u. U_ x e. z ( { ~P x , U. x } u. ran ( y e. z |-> { x , y } ) ) ) ) , ( A u. 1o ) ) |` _om ) ) -> E. u e. WUni A C_ u )
6 3 5 syl 
 |-  ( A e. V -> E. u e. WUni A C_ u )