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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 < 𝐵 ↔ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 <ℝ 𝐵 ) ∨ ( 𝐴 = -∞ ∧ 𝐵 = +∞ ) ) ∨ ( ( 𝐴 ∈ ℝ ∧ 𝐵 = +∞ ) ∨ ( 𝐴 = -∞ ∧ 𝐵 ∈ ℝ ) ) ) ) )