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 } )