Theorem wunint

Description: A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion	wunint	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3	1	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝑈 ∈ WUni )
4	1 2	wununi	⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑈 )
5	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∪ 𝐴 ∈ 𝑈 )
6		intssuni	⊢ ( 𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴 )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ⊆ ∪ 𝐴 )
8	3 5 7	wunss	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝑈 )