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 )