This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> U e. WUni )
wuncn.2 
|- ( ph -> _om e. U )
Assertion wuncn 
|- ( ph -> CC e. U )

Proof

Step Hyp Ref Expression
1 wuncn.1 
 |-  ( ph -> U e. WUni )
2 wuncn.2 
 |-  ( ph -> _om e. U )
3 df-c 
 |-  CC = ( R. X. R. )
4 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
5 df-ni 
 |-  N. = ( _om \ { (/) } )
6 1 2 wundif 
 |-  ( ph -> ( _om \ { (/) } ) e. U )
7 5 6 eqeltrid 
 |-  ( ph -> N. e. U )
8 1 7 7 wunxp 
 |-  ( ph -> ( N. X. N. ) e. U )
9 elpqn 
 |-  ( x e. Q. -> x e. ( N. X. N. ) )
10 9 ssriv 
 |-  Q. C_ ( N. X. N. )
11 10 a1i 
 |-  ( ph -> Q. C_ ( N. X. N. ) )
12 1 8 11 wunss 
 |-  ( ph -> Q. e. U )
13 1 12 wunpw 
 |-  ( ph -> ~P Q. e. U )
14 prpssnq 
 |-  ( x e. P. -> x C. Q. )
15 14 pssssd 
 |-  ( x e. P. -> x C_ Q. )
16 velpw 
 |-  ( x e. ~P Q. <-> x C_ Q. )
17 15 16 sylibr 
 |-  ( x e. P. -> x e. ~P Q. )
18 17 ssriv 
 |-  P. C_ ~P Q.
19 18 a1i 
 |-  ( ph -> P. C_ ~P Q. )
20 1 13 19 wunss 
 |-  ( ph -> P. e. U )
21 1 20 20 wunxp 
 |-  ( ph -> ( P. X. P. ) e. U )
22 1 21 wunpw 
 |-  ( ph -> ~P ( P. X. P. ) e. U )
23 enrer 
 |-  ~R Er ( P. X. P. )
24 23 a1i 
 |-  ( ph -> ~R Er ( P. X. P. ) )
25 24 qsss 
 |-  ( ph -> ( ( P. X. P. ) /. ~R ) C_ ~P ( P. X. P. ) )
26 1 22 25 wunss 
 |-  ( ph -> ( ( P. X. P. ) /. ~R ) e. U )
27 4 26 eqeltrid 
 |-  ( ph -> R. e. U )
28 1 27 27 wunxp 
 |-  ( ph -> ( R. X. R. ) e. U )
29 3 28 eqeltrid 
 |-  ( ph -> CC e. U )