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 ( 𝜑𝑈 ∈ 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 ( 𝜑 → ℂ ∈ 𝑈 )