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 φUWUni
wuncn.2 φωU
Assertion wuncn φU

Proof

Step Hyp Ref Expression
1 wuncn.1 φUWUni
2 wuncn.2 φωU
3 df-c =𝑹×𝑹
4 df-nr 𝑹=𝑷×𝑷/~𝑹
5 df-ni 𝑵=ω
6 1 2 wundif φωU
7 5 6 eqeltrid φ𝑵U
8 1 7 7 wunxp φ𝑵×𝑵U
9 elpqn x𝑸x𝑵×𝑵
10 9 ssriv 𝑸𝑵×𝑵
11 10 a1i φ𝑸𝑵×𝑵
12 1 8 11 wunss φ𝑸U
13 1 12 wunpw φ𝒫𝑸U
14 prpssnq x𝑷x𝑸
15 14 pssssd x𝑷x𝑸
16 velpw x𝒫𝑸x𝑸
17 15 16 sylibr x𝑷x𝒫𝑸
18 17 ssriv 𝑷𝒫𝑸
19 18 a1i φ𝑷𝒫𝑸
20 1 13 19 wunss φ𝑷U
21 1 20 20 wunxp φ𝑷×𝑷U
22 1 21 wunpw φ𝒫𝑷×𝑷U
23 enrer ~𝑹Er𝑷×𝑷
24 23 a1i φ~𝑹Er𝑷×𝑷
25 24 qsss φ𝑷×𝑷/~𝑹𝒫𝑷×𝑷
26 1 22 25 wunss φ𝑷×𝑷/~𝑹U
27 4 26 eqeltrid φ𝑹U
28 1 27 27 wunxp φ𝑹×𝑹U
29 3 28 eqeltrid φU