Metamath Proof Explorer


Theorem ltxr

Description: The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of Gleason p. 173. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion ltxr ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ∨ ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 breq12 ( ( 𝑥 = 𝐴𝑦 = 𝐵 ) → ( 𝑥 < 𝑦𝐴 < 𝐵 ) )
2 df-3an ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 < 𝑦 ) )
3 2 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 < 𝑦 ) }
4 1 3 brab2a ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } 𝐵 ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) )
5 4 a1i ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } 𝐵 ↔ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ) )
6 brun ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ↔ ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵𝐴 ( { -∞ } × ℝ ) 𝐵 ) )
7 brxp ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 ↔ ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ∧ 𝐵 ∈ { +∞ } ) )
8 elun ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 ∈ { -∞ } ) )
9 orcom ( ( 𝐴 ∈ ℝ ∨ 𝐴 ∈ { -∞ } ) ↔ ( 𝐴 ∈ { -∞ } ∨ 𝐴 ∈ ℝ ) )
10 8 9 bitri ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ↔ ( 𝐴 ∈ { -∞ } ∨ 𝐴 ∈ ℝ ) )
11 elsng ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ { -∞ } ↔ 𝐴 = -∞ ) )
12 11 orbi1d ( 𝐴 ∈ ℝ* → ( ( 𝐴 ∈ { -∞ } ∨ 𝐴 ∈ ℝ ) ↔ ( 𝐴 = -∞ ∨ 𝐴 ∈ ℝ ) ) )
13 10 12 syl5bb ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ↔ ( 𝐴 = -∞ ∨ 𝐴 ∈ ℝ ) ) )
14 elsng ( 𝐵 ∈ ℝ* → ( 𝐵 ∈ { +∞ } ↔ 𝐵 = +∞ ) )
15 13 14 bi2anan9 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ∧ 𝐵 ∈ { +∞ } ) ↔ ( ( 𝐴 = -∞ ∨ 𝐴 ∈ ℝ ) ∧ 𝐵 = +∞ ) ) )
16 andir ( ( ( 𝐴 = -∞ ∨ 𝐴 ∈ ℝ ) ∧ 𝐵 = +∞ ) ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ) )
17 15 16 bitrdi ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ∈ ( ℝ ∪ { -∞ } ) ∧ 𝐵 ∈ { +∞ } ) ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ) ) )
18 7 17 syl5bb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵 ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ) ) )
19 brxp ( 𝐴 ( { -∞ } × ℝ ) 𝐵 ↔ ( 𝐴 ∈ { -∞ } ∧ 𝐵 ∈ ℝ ) )
20 11 anbi1d ( 𝐴 ∈ ℝ* → ( ( 𝐴 ∈ { -∞ } ∧ 𝐵 ∈ ℝ ) ↔ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) )
21 20 adantr ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ∈ { -∞ } ∧ 𝐵 ∈ ℝ ) ↔ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) )
22 19 21 syl5bb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 ( { -∞ } × ℝ ) 𝐵 ↔ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) )
23 18 22 orbi12d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵𝐴 ( { -∞ } × ℝ ) 𝐵 ) ↔ ( ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) )
24 orass ( ( ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) )
25 23 24 bitrdi ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 ( ( ℝ ∪ { -∞ } ) × { +∞ } ) 𝐵𝐴 ( { -∞ } × ℝ ) 𝐵 ) ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )
26 6 25 syl5bb ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ↔ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )
27 5 26 orbi12d ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } 𝐵𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ∨ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) ) )
28 df-ltxr < = ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) )
29 28 breqi ( 𝐴 < 𝐵𝐴 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ) 𝐵 )
30 brun ( 𝐴 ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } ∪ ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) ) 𝐵 ↔ ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } 𝐵𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ) )
31 29 30 bitri ( 𝐴 < 𝐵 ↔ ( 𝐴 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ) } 𝐵𝐴 ( ( ( ℝ ∪ { -∞ } ) × { +∞ } ) ∪ ( { -∞ } × ℝ ) ) 𝐵 ) )
32 orass ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ∨ ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ↔ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ∨ ( ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )
33 27 31 32 3bitr4g ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 < 𝐵 ) ∨ ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )