Theorem wunco

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

	Ref	Expression
Hypotheses	wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunop.2	$$⊢\phi \to A\in U$$
	wunco.3	$$⊢\phi \to B\in U$$
Assertion	wunco	$$⊢\phi \to A\circ B\in U$$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wunop.2	$$⊢\phi \to A\in U$$
3		wunco.3	$$⊢\phi \to B\in U$$
4	1 3	wundm	$$⊢\phi \to \mathrm{dom}B\in U$$
5		dmcoss	$$⊢\mathrm{dom}\left(A\circ B\right)\subseteq \mathrm{dom}B$$
6	5	a1i	$$⊢\phi \to \mathrm{dom}\left(A\circ B\right)\subseteq \mathrm{dom}B$$
7	1 4 6	wunss	$$⊢\phi \to \mathrm{dom}\left(A\circ B\right)\in U$$
8	1 2	wunrn	$$⊢\phi \to \mathrm{ran}A\in U$$
9		rncoss	$$⊢\mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{ran}A$$
10	9	a1i	$$⊢\phi \to \mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{ran}A$$
11	1 8 10	wunss	$$⊢\phi \to \mathrm{ran}\left(A\circ B\right)\in U$$
12	1 7 11	wunxp	$$⊢\phi \to \mathrm{dom}\left(A\circ B\right)\times \mathrm{ran}\left(A\circ B\right)\in U$$
13		relco	$$⊢\mathrm{Rel}\left(A\circ B\right)$$
14		relssdmrn	$$⊢\mathrm{Rel}\left(A\circ B\right)\to A\circ B\subseteq \mathrm{dom}\left(A\circ B\right)\times \mathrm{ran}\left(A\circ B\right)$$
15	13 14	mp1i	$$⊢\phi \to A\circ B\subseteq \mathrm{dom}\left(A\circ B\right)\times \mathrm{ran}\left(A\circ B\right)$$
16	1 12 15	wunss	$$⊢\phi \to A\circ B\in U$$