Theorem wunco

Description: A weak universe is closed under composition. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	wun0.1	|- ( ph -> U e. WUni )
	wunop.2	|- ( ph -> A e. U )
	wunco.3	|- ( ph -> B e. U )
Assertion	wunco	|- ( ph -> ( A o. B ) e. U )

Proof

Step	Hyp	Ref	Expression
1		wun0.1	|- ( ph -> U e. WUni )
2		wunop.2	|- ( ph -> A e. U )
3		wunco.3	|- ( ph -> B e. U )
4	1 3	wundm	|- ( ph -> dom B e. U )
5		dmcoss	|- dom ( A o. B ) C_ dom B
6	5	a1i	|- ( ph -> dom ( A o. B ) C_ dom B )
7	1 4 6	wunss	|- ( ph -> dom ( A o. B ) e. U )
8	1 2	wunrn	|- ( ph -> ran A e. U )
9		rncoss	|- ran ( A o. B ) C_ ran A
10	9	a1i	|- ( ph -> ran ( A o. B ) C_ ran A )
11	1 8 10	wunss	|- ( ph -> ran ( A o. B ) e. U )
12	1 7 11	wunxp	|- ( ph -> ( dom ( A o. B ) X. ran ( A o. B ) ) e. U )
13		relco	|- Rel ( A o. B )
14		relssdmrn	|- ( Rel ( A o. B ) -> ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) )
15	13 14	mp1i	|- ( ph -> ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) )
16	1 12 15	wunss	|- ( ph -> ( A o. B ) e. U )