Theorem cnso

Description: The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Assertion	cnso	⊢ ∃ 𝑥 𝑥 Or ℂ

Proof

Step	Hyp	Ref	Expression
1		ltso	⊢ < Or ℝ
2		eqid	⊢ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } = { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) }
3		f1oiso	⊢ ( ( 𝑎 : ℝ –1-1-onto→ ℂ ∧ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } = { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ) → 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) )
4	2 3	mpan2	⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) )
5		isoso	⊢ ( 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) → ( < Or ℝ ↔ { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } Or ℂ ) )
6		soinxp	⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } Or ℂ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ )
7	5 6	bitrdi	⊢ ( 𝑎 Isom < , { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ( ℝ , ℂ ) → ( < Or ℝ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
8	4 7	syl	⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ( < Or ℝ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
9	1 8	mpbii	⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ )
10		cnex	⊢ ℂ ∈ V
11	10 10	xpex	⊢ ( ℂ × ℂ ) ∈ V
12	11	inex2	⊢ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) ∈ V
13		soeq1	⊢ ( 𝑥 = ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) → ( 𝑥 Or ℂ ↔ ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ ) )
14	12 13	spcev	⊢ ( ( { ⟨ 𝑏 , 𝑐 ⟩ ∣ ∃ 𝑑 ∈ ℝ ∃ 𝑒 ∈ ℝ ( ( 𝑏 = ( 𝑎 ‘ 𝑑 ) ∧ 𝑐 = ( 𝑎 ‘ 𝑒 ) ) ∧ 𝑑 < 𝑒 ) } ∩ ( ℂ × ℂ ) ) Or ℂ → ∃ 𝑥 𝑥 Or ℂ )
15	9 14	syl	⊢ ( 𝑎 : ℝ –1-1-onto→ ℂ → ∃ 𝑥 𝑥 Or ℂ )
16		rpnnen	⊢ ℝ ≈ 𝒫 ℕ
17		cpnnen	⊢ ℂ ≈ 𝒫 ℕ
18	16 17	entr4i	⊢ ℝ ≈ ℂ
19		bren	⊢ ( ℝ ≈ ℂ ↔ ∃ 𝑎 𝑎 : ℝ –1-1-onto→ ℂ )
20	18 19	mpbi	⊢ ∃ 𝑎 𝑎 : ℝ –1-1-onto→ ℂ
21	15 20	exlimiiv	⊢ ∃ 𝑥 𝑥 Or ℂ