cnso

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

		Ref	Expression
	Assertion	cnso	$⊢ \exists x x Or ℂ$

Proof

Step	Hyp	Ref	Expression
1		ltso	$⊢ < Or ℝ$
2		eqid	$⊢ \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} = \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}$
3		f1oiso	$⊢ (a : ℝ \underset{1-1 onto}{⟶} ℂ \land \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} = \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}) \to a {Isom}_{<, \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}} (ℝ, ℂ)$
4	2 3	mpan2	$⊢ a : ℝ \underset{1-1 onto}{⟶} ℂ \to a {Isom}_{<, \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}} (ℝ, ℂ)$
5		isoso	$⊢ a {Isom}_{<, \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}} (ℝ, ℂ) \to (< Or ℝ \leftrightarrow \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} Or ℂ)$
6		soinxp	$⊢ \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} Or ℂ \leftrightarrow (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ$
7	5 6	bitrdi	$⊢ a {Isom}_{<, \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\}} (ℝ, ℂ) \to (< Or ℝ \leftrightarrow (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ)$
8	4 7	syl	$⊢ a : ℝ \underset{1-1 onto}{⟶} ℂ \to (< Or ℝ \leftrightarrow (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ)$
9	1 8	mpbii	$⊢ a : ℝ \underset{1-1 onto}{⟶} ℂ \to (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ$
10		cnex	$⊢ ℂ \in V$
11	10 10	xpex	$⊢ ℂ \times ℂ \in V$
12	11	inex2	$⊢ \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ) \in V$
13		soeq1	$⊢ x = \{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ) \to (x Or ℂ \leftrightarrow (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ)$
14	12 13	spcev	$⊢ (\{⟨b, c⟩ \| \exists d \in ℝ \exists e \in ℝ ((b = a (d) \land c = a (e)) \land d < e)\} \cap (ℂ \times ℂ)) Or ℂ \to \exists x x Or ℂ$
15	9 14	syl	$⊢ a : ℝ \underset{1-1 onto}{⟶} ℂ \to \exists x x Or ℂ$
16		rpnnen	$⊢ ℝ \approx 𝒫 ℕ$
17		cpnnen	$⊢ ℂ \approx 𝒫 ℕ$
18	16 17	entr4i	$⊢ ℝ \approx ℂ$
19		bren	$⊢ ℝ \approx ℂ \leftrightarrow \exists a a : ℝ \underset{1-1 onto}{⟶} ℂ$
20	18 19	mpbi	$⊢ \exists a a : ℝ \underset{1-1 onto}{⟶} ℂ$
21	15 20	exlimiiv	$⊢ \exists x x Or ℂ$

Metamath Proof Explorer

Theorem cnso

Proof