ltresr

Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltresr	⊢ ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ 𝐴 <_R 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ltrelre	⊢ <_ℝ ⊆ ( ℝ × ℝ )
2	1	brel	⊢ ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ → ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) )
3		opelreal	⊢ ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ↔ 𝐴 ∈ R )
4		opelreal	⊢ ( ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ↔ 𝐵 ∈ R )
5	3 4	anbi12i	⊢ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) ↔ ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )
6	2 5	sylib	⊢ ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ → ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )
7		ltrelsr	⊢ <_R ⊆ ( R × R )
8	7	brel	⊢ ( 𝐴 <_R 𝐵 → ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) )
9		opex	⊢ ⟨ 𝐴 , 0_R ⟩ ∈ V
10		opex	⊢ ⟨ 𝐵 , 0_R ⟩ ∈ V
11		eleq1	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( 𝑥 ∈ ℝ ↔ ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ) )
12	11	anbi1d	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ↔ ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) )
13		eqeq1	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ↔ ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ) )
14	13	anbi1d	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ↔ ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ) )
15	14	anbi1d	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( ( ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
16	15	2exbidv	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
17	12 16	anbi12d	⊢ ( 𝑥 = ⟨ 𝐴 , 0_R ⟩ → ( ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) ↔ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) ) )
18		eleq1	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( 𝑦 ∈ ℝ ↔ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) )
19	18	anbi2d	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ↔ ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) ) )
20		eqeq1	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( 𝑦 = ⟨ 𝑤 , 0_R ⟩ ↔ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) )
21	20	anbi2d	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ↔ ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ) )
22	21	anbi1d	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
23	22	2exbidv	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
24	19 23	anbi12d	⊢ ( 𝑦 = ⟨ 𝐵 , 0_R ⟩ → ( ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) ↔ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) ) )
25		df-lt	⊢ <_ℝ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = ⟨ 𝑧 , 0_R ⟩ ∧ 𝑦 = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) }
26	9 10 17 24 25	brab	⊢ ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) ∧ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
27	26	baib	⊢ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) → ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ) )
28		vex	⊢ 𝑧 ∈ V
29	28	eqresr	⊢ ( ⟨ 𝑧 , 0_R ⟩ = ⟨ 𝐴 , 0_R ⟩ ↔ 𝑧 = 𝐴 )
30		eqcom	⊢ ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ↔ ⟨ 𝑧 , 0_R ⟩ = ⟨ 𝐴 , 0_R ⟩ )
31		eqcom	⊢ ( 𝐴 = 𝑧 ↔ 𝑧 = 𝐴 )
32	29 30 31	3bitr4i	⊢ ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ↔ 𝐴 = 𝑧 )
33		vex	⊢ 𝑤 ∈ V
34	33	eqresr	⊢ ( ⟨ 𝑤 , 0_R ⟩ = ⟨ 𝐵 , 0_R ⟩ ↔ 𝑤 = 𝐵 )
35		eqcom	⊢ ( ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ↔ ⟨ 𝑤 , 0_R ⟩ = ⟨ 𝐵 , 0_R ⟩ )
36		eqcom	⊢ ( 𝐵 = 𝑤 ↔ 𝑤 = 𝐵 )
37	34 35 36	3bitr4i	⊢ ( ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ↔ 𝐵 = 𝑤 )
38	32 37	anbi12i	⊢ ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ↔ ( 𝐴 = 𝑧 ∧ 𝐵 = 𝑤 ) )
39	28 33	opth2	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ↔ ( 𝐴 = 𝑧 ∧ 𝐵 = 𝑤 ) )
40	38 39	bitr4i	⊢ ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ )
41	40	anbi1i	⊢ ( ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 <_R 𝑤 ) )
42	41	2exbii	⊢ ( ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 0_R ⟩ = ⟨ 𝑧 , 0_R ⟩ ∧ ⟨ 𝐵 , 0_R ⟩ = ⟨ 𝑤 , 0_R ⟩ ) ∧ 𝑧 <_R 𝑤 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 <_R 𝑤 ) )
43	27 42	bitrdi	⊢ ( ( ⟨ 𝐴 , 0_R ⟩ ∈ ℝ ∧ ⟨ 𝐵 , 0_R ⟩ ∈ ℝ ) → ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 <_R 𝑤 ) ) )
44	3 4 43	syl2anbr	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 <_R 𝑤 ) ) )
45		breq12	⊢ ( ( 𝑧 = 𝐴 ∧ 𝑤 = 𝐵 ) → ( 𝑧 <_R 𝑤 ↔ 𝐴 <_R 𝐵 ) )
46	45	copsex2g	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ∃ 𝑧 ∃ 𝑤 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ∧ 𝑧 <_R 𝑤 ) ↔ 𝐴 <_R 𝐵 ) )
47	44 46	bitrd	⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ 𝐴 <_R 𝐵 ) )
48	6 8 47	pm5.21nii	⊢ ( ⟨ 𝐴 , 0_R ⟩ <_ℝ ⟨ 𝐵 , 0_R ⟩ ↔ 𝐴 <_R 𝐵 )

Metamath Proof Explorer

Theorem ltresr

Proof