Theorem wunccl

Description: The weak universe closure of a set is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	wunccl	⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ∈ WUni )

Proof

Step	Hyp	Ref	Expression
1		wuncval	⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) = ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } )
2		ssrab2	⊢ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ⊆ WUni
3		wunex	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 )
4		rabn0	⊢ ( { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ ↔ ∃ 𝑢 ∈ WUni 𝐴 ⊆ 𝑢 )
5	3 4	sylibr	⊢ ( 𝐴 ∈ 𝑉 → { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ )
6		intwun	⊢ ( ( { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ⊆ WUni ∧ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ≠ ∅ ) → ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ∈ WUni )
7	2 5 6	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ∩ { 𝑢 ∈ WUni ∣ 𝐴 ⊆ 𝑢 } ∈ WUni )
8	1 7	eqeltrd	⊢ ( 𝐴 ∈ 𝑉 → ( wUniCl ‘ 𝐴 ) ∈ WUni )