Theorem wunint

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

	Ref	Expression
Hypotheses	wununi.1	|- ( ph -> U e. WUni )
	wununi.2	|- ( ph -> A e. U )
Assertion	wunint	|- ( ( ph /\ A =/= (/) ) -> |^| A e. U )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	|- ( ph -> U e. WUni )
2		wununi.2	|- ( ph -> A e. U )
3	1	adantr	|- ( ( ph /\ A =/= (/) ) -> U e. WUni )
4	1 2	wununi	|- ( ph -> U. A e. U )
5	4	adantr	|- ( ( ph /\ A =/= (/) ) -> U. A e. U )
6		intssuni	|- ( A =/= (/) -> |^| A C_ U. A )
7	6	adantl	|- ( ( ph /\ A =/= (/) ) -> |^| A C_ U. A )
8	3 5 7	wunss	|- ( ( ph /\ A =/= (/) ) -> |^| A e. U )