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 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 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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵𝐴 < 𝐵 ) )