Metamath Proof Explorer

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 ${⊢}ℂ=𝑹×𝑹$
4 df-nr ${⊢}𝑹=\left(𝑷×𝑷\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 𝑵×𝑵\in {U}$
9 elpqn ${⊢}{x}\in 𝑸\to {x}\in \left(𝑵×𝑵\right)$
10 9 ssriv ${⊢}𝑸\subseteq 𝑵×𝑵$
11 10 a1i ${⊢}{\phi }\to 𝑸\subseteq 𝑵×𝑵$
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 𝒫𝑸↔{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 𝑷×𝑷\in {U}$
22 1 21 wunpw ${⊢}{\phi }\to 𝒫\left(𝑷×𝑷\right)\in {U}$
23 enrer ${⊢}{~}_{𝑹}\mathrm{Er}\left(𝑷×𝑷\right)$
24 23 a1i ${⊢}{\phi }\to {~}_{𝑹}\mathrm{Er}\left(𝑷×𝑷\right)$
25 24 qsss ${⊢}{\phi }\to \left(𝑷×𝑷\right)/{~}_{𝑹}\subseteq 𝒫\left(𝑷×𝑷\right)$
26 1 22 25 wunss ${⊢}{\phi }\to \left(𝑷×𝑷\right)/{~}_{𝑹}\in {U}$
27 4 26 eqeltrid ${⊢}{\phi }\to 𝑹\in {U}$
28 1 27 27 wunxp ${⊢}{\phi }\to 𝑹×𝑹\in {U}$
29 3 28 eqeltrid ${⊢}{\phi }\to ℂ\in {U}$