Definition df-ltr

Description: Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.4 of Gleason p. 127. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ltr	⊢ <R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltr	⊢ <R
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4		cnr	⊢ R
5	3 4	wcel	⊢ 𝑥 ∈ R
6	2	cv	⊢ 𝑦
7	6 4	wcel	⊢ 𝑦 ∈ R
8	5 7	wa	⊢ ( 𝑥 ∈ R ∧ 𝑦 ∈ R )
9		vz	⊢ 𝑧
10		vw	⊢ 𝑤
11		vv	⊢ 𝑣
12		vu	⊢ 𝑢
13	9	cv	⊢ 𝑧
14	10	cv	⊢ 𝑤
15	13 14	cop	⊢ ⟨ 𝑧 , 𝑤 ⟩
16		cer	⊢ ~R
17	15 16	cec	⊢ [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R
18	3 17	wceq	⊢ 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R
19	11	cv	⊢ 𝑣
20	12	cv	⊢ 𝑢
21	19 20	cop	⊢ ⟨ 𝑣 , 𝑢 ⟩
22	21 16	cec	⊢ [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R
23	6 22	wceq	⊢ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R
24	18 23	wa	⊢ ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R )
25		cpp	⊢ +P
26	13 20 25	co	⊢ ( 𝑧 +P 𝑢 )
27		cltp	⊢ <P
28	14 19 25	co	⊢ ( 𝑤 +P 𝑣 )
29	26 28 27	wbr	⊢ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 )
30	24 29	wa	⊢ ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
31	30 12	wex	⊢ ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
32	31 11	wex	⊢ ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
33	32 10	wex	⊢ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
34	33 9	wex	⊢ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) )
35	8 34	wa	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) )
36	35 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) ) }
37	0 36	wceq	⊢ <R = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ R ) ∧ ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ∧ 𝑦 = [ ⟨ 𝑣 , 𝑢 ⟩ ] ~R ) ∧ ( 𝑧 +P 𝑢 ) <P ( 𝑤 +P 𝑣 ) ) ) }