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	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wuncn.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
Assertion	wuncn	⊢ ( 𝜑 → ℂ ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wuncn.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wuncn.2	⊢ ( 𝜑 → ω ∈ 𝑈 )
3		df-c	⊢ ℂ = ( R × R )
4		df-nr	⊢ R = ( ( P × P ) / ~R )
5		df-ni	⊢ N = ( ω ∖ { ∅ } )
6	1 2	wundif	⊢ ( 𝜑 → ( ω ∖ { ∅ } ) ∈ 𝑈 )
7	5 6	eqeltrid	⊢ ( 𝜑 → N ∈ 𝑈 )
8	1 7 7	wunxp	⊢ ( 𝜑 → ( N × N ) ∈ 𝑈 )
9		elpqn	⊢ ( 𝑥 ∈ Q → 𝑥 ∈ ( N × N ) )
10	9	ssriv	⊢ Q ⊆ ( N × N )
11	10	a1i	⊢ ( 𝜑 → Q ⊆ ( N × N ) )
12	1 8 11	wunss	⊢ ( 𝜑 → Q ∈ 𝑈 )
13	1 12	wunpw	⊢ ( 𝜑 → 𝒫 Q ∈ 𝑈 )
14		prpssnq	⊢ ( 𝑥 ∈ P → 𝑥 ⊊ Q )
15	14	pssssd	⊢ ( 𝑥 ∈ P → 𝑥 ⊆ Q )
16		velpw	⊢ ( 𝑥 ∈ 𝒫 Q ↔ 𝑥 ⊆ Q )
17	15 16	sylibr	⊢ ( 𝑥 ∈ P → 𝑥 ∈ 𝒫 Q )
18	17	ssriv	⊢ P ⊆ 𝒫 Q
19	18	a1i	⊢ ( 𝜑 → P ⊆ 𝒫 Q )
20	1 13 19	wunss	⊢ ( 𝜑 → P ∈ 𝑈 )
21	1 20 20	wunxp	⊢ ( 𝜑 → ( P × P ) ∈ 𝑈 )
22	1 21	wunpw	⊢ ( 𝜑 → 𝒫 ( P × P ) ∈ 𝑈 )
23		enrer	⊢ ~R Er ( P × P )
24	23	a1i	⊢ ( 𝜑 → ~R Er ( P × P ) )
25	24	qsss	⊢ ( 𝜑 → ( ( P × P ) / ~R ) ⊆ 𝒫 ( P × P ) )
26	1 22 25	wunss	⊢ ( 𝜑 → ( ( P × P ) / ~R ) ∈ 𝑈 )
27	4 26	eqeltrid	⊢ ( 𝜑 → R ∈ 𝑈 )
28	1 27 27	wunxp	⊢ ( 𝜑 → ( R × R ) ∈ 𝑈 )
29	3 28	eqeltrid	⊢ ( 𝜑 → ℂ ∈ 𝑈 )