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 ∈ V → wUniCl ⁡ A = ⋂ u ∈ WUni | A ⊆ u

Proof

Step Hyp Ref Expression
1 df-wunc ⊢ wUniCl = x ∈ V ⟼ ⋂ u ∈ WUni | x ⊆ u
2 sseq1 ⊢ x = A → x ⊆ u ↔ A ⊆ u
3 2 rabbidv ⊢ x = A → u ∈ WUni | x ⊆ u = u ∈ WUni | A ⊆ u
4 3 inteqd ⊢ x = A → ⋂ u ∈ WUni | x ⊆ u = ⋂ u ∈ WUni | A ⊆ u
5 elex ⊢ A ∈ V → A ∈ V
6 wunex ⊢ A ∈ V → ∃ u ∈ WUni A ⊆ u
7 rabn0 ⊢ u ∈ WUni | A ⊆ u ≠ ∅ ↔ ∃ u ∈ WUni A ⊆ u
8 6 7 sylibr ⊢ A ∈ V → u ∈ WUni | A ⊆ u ≠ ∅
9 intex ⊢ u ∈ WUni | A ⊆ u ≠ ∅ ↔ ⋂ u ∈ WUni | A ⊆ u ∈ V
10 8 9 sylib ⊢ A ∈ V → ⋂ u ∈ WUni | A ⊆ u ∈ V
11 1 4 5 10 fvmptd3 ⊢ A ∈ V → wUniCl ⁡ A = ⋂ u ∈ WUni | A ⊆ u