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