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

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 ∣ 𝐴 ⊆ 𝑢 } )