Metamath Proof Explorer

Theorem wuncval

Description: Value of the weak universe closure operator. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion wuncval 
|- ( A e. V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )

Proof

Step Hyp Ref Expression
1 df-wunc 
 |-  wUniCl = ( x e. _V |-> |^| { u e. WUni | x C_ u } )
2 sseq1 
 |-  ( x = A -> ( x C_ u <-> A C_ u ) )
3 2 rabbidv 
 |-  ( x = A -> { u e. WUni | x C_ u } = { u e. WUni | A C_ u } )
4 3 inteqd 
 |-  ( x = A -> |^| { u e. WUni | x C_ u } = |^| { u e. WUni | A C_ u } )
5 elex 
 |-  ( A e. V -> A e. _V )
6 wunex 
 |-  ( A e. V -> E. u e. WUni A C_ u )
7 rabn0 
 |-  ( { u e. WUni | A C_ u } =/= (/) <-> E. u e. WUni A C_ u )
8 6 7 sylibr 
 |-  ( A e. V -> { u e. WUni | A C_ u } =/= (/) )
9 intex 
 |-  ( { u e. WUni | A C_ u } =/= (/) <-> |^| { u e. WUni | A C_ u } e. _V )
10 8 9 sylib 
 |-  ( A e. V -> |^| { u e. WUni | A C_ u } e. _V )
11 1 4 5 10 fvmptd3 
 |-  ( A e. V -> ( wUniCl ` A ) = |^| { u e. WUni | A C_ u } )