This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 imbitrid ⊢ ( 𝐵 = +∞ → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → +∞ ∈ ℝ ) )
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 imbitrid ⊢ ( 𝐴 = -∞ → ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → -∞ ∈ ℝ ) )
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 df-ltxr ⊢ < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )
27 26 equncomi ⊢ < = ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } )
28 27 breqi ⊢ ( 𝐴 < 𝐵 ↔ 𝐴 ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ) 𝐵 )
29 brun ⊢ ( 𝐴 ( ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } ) 𝐵 ↔ ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ∨ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
30 df-or ⊢ ( ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ∨ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
31 28 29 30 3bitri ⊢ ( 𝐴 < 𝐵 ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
32 biimt ⊢ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ↔ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) ) )
33 31 32 bitr4id ⊢ ( ¬ 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 → ( 𝐴 < 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
34 25 33 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
35 breq12 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 <ℝ 𝑦 ↔ 𝐴 <ℝ 𝐵 ) )
36 df-3an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) )
37 36 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 <ℝ 𝑦 ) }
38 35 37 brab2a ⊢ ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 <ℝ 𝐵 ) )
39 38 baibr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <ℝ 𝐵 ↔ 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 <ℝ 𝑦 ) } 𝐵 ) )
40 34 39 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 <ℝ 𝐵 ) )