Theorem ltxrlt

Description: The standard less-than and the extended real less-than < are identical when restricted to the non-extended reals RR . (Contributed by NM, 13-Oct-2005) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	ltxrlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brun	⊢ ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ↔ ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 ∨ 𝐴 ( { -∞ } × ℝ ) 𝐵 ) )
2		brxp	⊢ ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 ↔ ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ∧ 𝐵 ∈ { +∞ } ) )
3		elsni	⊢ ( 𝐵 ∈ { +∞ } → 𝐵 = +∞ )
4		pnfnre	⊢ +∞ ∉ ℝ
5	4	neli	⊢ ¬ +∞ ∈ ℝ
6		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
7		eleq1	⊢ ( 𝐵 = +∞ → ( 𝐵 ∈ ℝ ↔ +∞ ∈ ℝ ) )
8	6 7	syl5ib	⊢ ( 𝐵 = +∞ → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → +∞ ∈ ℝ ) )
9	5 8	mtoi	⊢ ( 𝐵 = +∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
10	3 9	syl	⊢ ( 𝐵 ∈ { +∞ } → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
11	2 10	simplbiim	⊢ ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
12		brxp	⊢ ( 𝐴 ( { -∞ } × ℝ ) 𝐵 ↔ ( 𝐴 ∈ { -∞ } ∧ 𝐵 ∈ ℝ ) )
13		elsni	⊢ ( 𝐴 ∈ { -∞ } → 𝐴 = -∞ )
14		mnfnre	⊢ -∞ ∉ ℝ
15	14	neli	⊢ ¬ -∞ ∈ ℝ
16		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
17		eleq1	⊢ ( 𝐴 = -∞ → ( 𝐴 ∈ ℝ ↔ -∞ ∈ ℝ ) )
18	16 17	syl5ib	⊢ ( 𝐴 = -∞ → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -∞ ∈ ℝ ) )
19	15 18	mtoi	⊢ ( 𝐴 = -∞ → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
20	13 19	syl	⊢ ( 𝐴 ∈ { -∞ } → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
21	20	adantr	⊢ ( ( 𝐴 ∈ { -∞ } ∧ 𝐵 ∈ ℝ ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
22	12 21	sylbi	⊢ ( 𝐴 ( { -∞ } × ℝ ) 𝐵 → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
23	11 22	jaoi	⊢ ( ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 ∨ 𝐴 ( { -∞ } × ℝ ) 𝐵 ) → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
24	1 23	sylbi	⊢ ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → ¬ ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
25	24	con2i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 )
26		biimt	⊢ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) ) )
27		df-ltxr	⊢ < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )
28	27	equncomi	⊢ < = ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } )
29	28	breqi	⊢ ( 𝐴 < 𝐵 ↔ 𝐴 ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ) 𝐵 )
30		brun	⊢ ( 𝐴 ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ) 𝐵 ↔ ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ∨ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
31		df-or	⊢ ( ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ∨ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
32	29 30 31	3bitri	⊢ ( 𝐴 < 𝐵 ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
33	26 32	syl6rbbr	⊢ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → ( 𝐴 < 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
34	25 33	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
35		breq12	⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵 ) )
36		df-3an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) )
37	36	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) }
38	35 37	brab2a	⊢ ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 <ℝ 𝐵 ) )
39	38	baibr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
40	34 39	bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) )