Theorem wundm

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

	Ref	Expression
Hypotheses	wun0.1	|- ( ph -> U e. WUni )
	wunop.2	|- ( ph -> A e. U )
Assertion	wundm	|- ( ph -> dom A e. U )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	|- ( ph -> U e. WUni )
2		wunop.2	|- ( ph -> A e. U )
3	1 2	wununi	|- ( ph -> U. A e. U )
4	1 3	wununi	|- ( ph -> U. U. A e. U )
5		ssun1	|- dom A C_ ( dom A u. ran A )
6		dmrnssfld	|- ( dom A u. ran A ) C_ U. U. A
7	5 6	sstri	|- dom A C_ U. U. A
8	7	a1i	|- ( ph -> dom A C_ U. U. A )
9	1 4 8	wunss	|- ( ph -> dom A e. U )