Metamath Proof Explorer


Theorem wuncval

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

Ref Expression
Assertion wuncval ( 𝐴𝑉 → ( wUniCl ‘ 𝐴 ) = { 𝑢 ∈ WUni ∣ 𝐴𝑢 } )

Proof

Step Hyp Ref Expression
1 df-wunc wUniCl = ( 𝑥 ∈ V ↦ { 𝑢 ∈ WUni ∣ 𝑥𝑢 } )
2 sseq1 ( 𝑥 = 𝐴 → ( 𝑥𝑢𝐴𝑢 ) )
3 2 rabbidv ( 𝑥 = 𝐴 → { 𝑢 ∈ WUni ∣ 𝑥𝑢 } = { 𝑢 ∈ WUni ∣ 𝐴𝑢 } )
4 3 inteqd ( 𝑥 = 𝐴 { 𝑢 ∈ WUni ∣ 𝑥𝑢 } = { 𝑢 ∈ WUni ∣ 𝐴𝑢 } )
5 elex ( 𝐴𝑉𝐴 ∈ V )
6 wunex ( 𝐴𝑉 → ∃ 𝑢 ∈ WUni 𝐴𝑢 )
7 rabn0 ( { 𝑢 ∈ WUni ∣ 𝐴𝑢 } ≠ ∅ ↔ ∃ 𝑢 ∈ WUni 𝐴𝑢 )
8 6 7 sylibr ( 𝐴𝑉 → { 𝑢 ∈ WUni ∣ 𝐴𝑢 } ≠ ∅ )
9 intex ( { 𝑢 ∈ WUni ∣ 𝐴𝑢 } ≠ ∅ ↔ { 𝑢 ∈ WUni ∣ 𝐴𝑢 } ∈ V )
10 8 9 sylib ( 𝐴𝑉 { 𝑢 ∈ WUni ∣ 𝐴𝑢 } ∈ V )
11 1 4 5 10 fvmptd3 ( 𝐴𝑉 → ( wUniCl ‘ 𝐴 ) = { 𝑢 ∈ WUni ∣ 𝐴𝑢 } )