Theorem wuncnv

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

	Ref	Expression
Hypotheses	wun0.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wunop.2	$$⊢\phi \to A\in U$$
Assertion	wuncnv	$$⊢\phi \to A^{-1}\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	1 2	wunrn	$$⊢\phi \to \mathrm{ran}A\in U$$
4	1 2	wundm	$$⊢\phi \to \mathrm{dom}A\in U$$
5	1 3 4	wunxp	$$⊢\phi \to \mathrm{ran}A\times \mathrm{dom}A\in U$$
6		cnvssrndm	$$⊢A^{-1}\subseteq \mathrm{ran}A\times \mathrm{dom}A$$
7	6	a1i	$$⊢\phi \to A^{-1}\subseteq \mathrm{ran}A\times \mathrm{dom}A$$
8	1 5 7	wunss	$$⊢\phi \to A^{-1}\in U$$