Theorem wuncn

Description: A weak universe containing _om contains the complex number construction. This theorem is construction-dependent in the literal sense, but will also be satisfied by any other reasonable implementation of the complex numbers. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wuncn.1	$$⊢\phi \to U\in \mathrm{WUni}$$
	wuncn.2	$$⊢\phi \to \mathrm{\omega }\in U$$
Assertion	wuncn	$$⊢\phi \to ℂ\in U$$

Proof

Step	Hyp	Ref	Expression
1		wuncn.1	$$⊢\phi \to U\in \mathrm{WUni}$$
2		wuncn.2	$$⊢\phi \to \mathrm{\omega }\in U$$
3		df-c	$$⊢ℂ=𝑹\times 𝑹$$
4		df-nr	$$⊢𝑹=\left(𝑷\times 𝑷\right)/{~}_{𝑹}$$
5		df-ni	$$⊢𝑵=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
6	1 2	wundif	$$⊢\phi \to \mathrm{\omega }\setminus \left\{\varnothing \right\}\in U$$
7	5 6	eqeltrid	$$⊢\phi \to 𝑵\in U$$
8	1 7 7	wunxp	$$⊢\phi \to 𝑵\times 𝑵\in U$$
9		elpqn	$$⊢x\in 𝑸\to x\in \left(𝑵\times 𝑵\right)$$
10	9	ssriv	$$⊢𝑸\subseteq 𝑵\times 𝑵$$
11	10	a1i	$$⊢\phi \to 𝑸\subseteq 𝑵\times 𝑵$$
12	1 8 11	wunss	$$⊢\phi \to 𝑸\in U$$
13	1 12	wunpw	$$⊢\phi \to 𝒫𝑸\in U$$
14		prpssnq	$$⊢x\in 𝑷\to x\subset 𝑸$$
15	14	pssssd	$$⊢x\in 𝑷\to x\subseteq 𝑸$$
16		velpw	$$⊢x\in 𝒫𝑸\leftrightarrow x\subseteq 𝑸$$
17	15 16	sylibr	$$⊢x\in 𝑷\to x\in 𝒫𝑸$$
18	17	ssriv	$$⊢𝑷\subseteq 𝒫𝑸$$
19	18	a1i	$$⊢\phi \to 𝑷\subseteq 𝒫𝑸$$
20	1 13 19	wunss	$$⊢\phi \to 𝑷\in U$$
21	1 20 20	wunxp	$$⊢\phi \to 𝑷\times 𝑷\in U$$
22	1 21	wunpw	$$⊢\phi \to 𝒫\left(𝑷\times 𝑷\right)\in U$$
23		enrer	$$⊢{~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$
24	23	a1i	$$⊢\phi \to {~}_{𝑹}\mathrm{Er}\left(𝑷\times 𝑷\right)$$
25	24	qsss	$$⊢\phi \to \left(𝑷\times 𝑷\right)/{~}_{𝑹}\subseteq 𝒫\left(𝑷\times 𝑷\right)$$
26	1 22 25	wunss	$$⊢\phi \to \left(𝑷\times 𝑷\right)/{~}_{𝑹}\in U$$
27	4 26	eqeltrid	$$⊢\phi \to 𝑹\in U$$
28	1 27 27	wunxp	$$⊢\phi \to 𝑹\times 𝑹\in U$$
29	3 28	eqeltrid	$$⊢\phi \to ℂ\in U$$