Theorem ltxr 8465

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.)

Assertion

Ref	Expression
ltxr	⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ ((((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ (A = -∞ ∧ B = +∞)) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))

Proof of Theorem ltxr

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq12 3760	. . . . 5 ⊢ ((x = A ∧ y = B) → (x <ℝ y ↔ A <ℝ B))
2		df-3an 886	. . . . . 6 ⊢ ((x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y) ↔ ((x ∈ ℝ ∧ y ∈ ℝ) ∧ x <ℝ y))
3	2	opabbii 3815	. . . . 5 ⊢ {⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)} = {⟨x, y⟩ ∣ ((x ∈ ℝ ∧ y ∈ ℝ) ∧ x <ℝ y)}
4	1, 3	brab2ga 4358	. . . 4 ⊢ (A{⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)}B ↔ ((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B))
5	4	a1i 9	. . 3 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A{⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)}B ↔ ((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B)))
6		brun 3801	. . . 4 ⊢ (A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B ↔ (A((ℝ ∪ {-∞}) × {+∞})B ∨ A({-∞} × ℝ)B))
7		brxp 4318	. . . . . . 7 ⊢ (A((ℝ ∪ {-∞}) × {+∞})B ↔ (A ∈ (ℝ ∪ {-∞}) ∧ B ∈ {+∞}))
8		elun 3078	. . . . . . . . . . 11 ⊢ (A ∈ (ℝ ∪ {-∞}) ↔ (A ∈ ℝ ∨ A ∈ {-∞}))
9		orcom 646	. . . . . . . . . . 11 ⊢ ((A ∈ ℝ ∨ A ∈ {-∞}) ↔ (A ∈ {-∞} ∨ A ∈ ℝ))
10	8, 9	bitri 173	. . . . . . . . . 10 ⊢ (A ∈ (ℝ ∪ {-∞}) ↔ (A ∈ {-∞} ∨ A ∈ ℝ))
11		elsncg 3389	. . . . . . . . . . 11 ⊢ (A ∈ ℝ* → (A ∈ {-∞} ↔ A = -∞))
12	11	orbi1d 704	. . . . . . . . . 10 ⊢ (A ∈ ℝ* → ((A ∈ {-∞} ∨ A ∈ ℝ) ↔ (A = -∞ ∨ A ∈ ℝ)))
13	10, 12	syl5bb 181	. . . . . . . . 9 ⊢ (A ∈ ℝ* → (A ∈ (ℝ ∪ {-∞}) ↔ (A = -∞ ∨ A ∈ ℝ)))
14		elsncg 3389	. . . . . . . . 9 ⊢ (B ∈ ℝ* → (B ∈ {+∞} ↔ B = +∞))
15	13, 14	bi2anan9 538	. . . . . . . 8 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ (ℝ ∪ {-∞}) ∧ B ∈ {+∞}) ↔ ((A = -∞ ∨ A ∈ ℝ) ∧ B = +∞)))
16		andir 731	. . . . . . . 8 ⊢ (((A = -∞ ∨ A ∈ ℝ) ∧ B = +∞) ↔ ((A = -∞ ∧ B = +∞) ∨ (A ∈ ℝ ∧ B = +∞)))
17	15, 16	syl6bb 185	. . . . . . 7 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ (ℝ ∪ {-∞}) ∧ B ∈ {+∞}) ↔ ((A = -∞ ∧ B = +∞) ∨ (A ∈ ℝ ∧ B = +∞))))
18	7, 17	syl5bb 181	. . . . . 6 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A((ℝ ∪ {-∞}) × {+∞})B ↔ ((A = -∞ ∧ B = +∞) ∨ (A ∈ ℝ ∧ B = +∞))))
19		brxp 4318	. . . . . . 7 ⊢ (A({-∞} × ℝ)B ↔ (A ∈ {-∞} ∧ B ∈ ℝ))
20	11	anbi1d 438	. . . . . . . 8 ⊢ (A ∈ ℝ* → ((A ∈ {-∞} ∧ B ∈ ℝ) ↔ (A = -∞ ∧ B ∈ ℝ)))
21	20	adantr 261	. . . . . . 7 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A ∈ {-∞} ∧ B ∈ ℝ) ↔ (A = -∞ ∧ B ∈ ℝ)))
22	19, 21	syl5bb 181	. . . . . 6 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A({-∞} × ℝ)B ↔ (A = -∞ ∧ B ∈ ℝ)))
23	18, 22	orbi12d 706	. . . . 5 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A((ℝ ∪ {-∞}) × {+∞})B ∨ A({-∞} × ℝ)B) ↔ (((A = -∞ ∧ B = +∞) ∨ (A ∈ ℝ ∧ B = +∞)) ∨ (A = -∞ ∧ B ∈ ℝ))))
24		orass 683	. . . . 5 ⊢ ((((A = -∞ ∧ B = +∞) ∨ (A ∈ ℝ ∧ B = +∞)) ∨ (A = -∞ ∧ B ∈ ℝ)) ↔ ((A = -∞ ∧ B = +∞) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ))))
25	23, 24	syl6bb 185	. . . 4 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A((ℝ ∪ {-∞}) × {+∞})B ∨ A({-∞} × ℝ)B) ↔ ((A = -∞ ∧ B = +∞) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))
26	6, 25	syl5bb 181	. . 3 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B ↔ ((A = -∞ ∧ B = +∞) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))
27	5, 26	orbi12d 706	. 2 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → ((A{⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)}B ∨ A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B) ↔ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ ((A = -∞ ∧ B = +∞) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ))))))
28		df-ltxr 6862	. . . 4 ⊢ < = ({⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
29	28	breqi 3761	. . 3 ⊢ (A < B ↔ A({⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))B)
30		brun 3801	. . 3 ⊢ (A({⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))B ↔ (A{⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)}B ∨ A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B))
31	29, 30	bitri 173	. 2 ⊢ (A < B ↔ (A{⟨x, y⟩ ∣ (x ∈ ℝ ∧ y ∈ ℝ ∧ x <ℝ y)}B ∨ A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B))
32		orass 683	. 2 ⊢ (((((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ (A = -∞ ∧ B = +∞)) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ))) ↔ (((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ ((A = -∞ ∧ B = +∞) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))
33	27, 31, 32	3bitr4g 212	1 ⊢ ((A ∈ ℝ* ∧ B ∈ ℝ*) → (A < B ↔ ((((A ∈ ℝ ∧ B ∈ ℝ) ∧ A <ℝ B) ∨ (A = -∞ ∧ B = +∞)) ∨ ((A ∈ ℝ ∧ B = +∞) ∨ (A = -∞ ∧ B ∈ ℝ)))))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390   ∪ cun 2909  {csn 3367   class class class wbr 3755  {copab 3808   × cxp 4286  ℝcr 6710   <_ℝ cltrr 6715  +∞cpnf 6854  -∞cmnf 6855  ℝ^*cxr 6856   < clt 6857

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-ltxr 6862

This theorem is referenced by:  xrltnr  8471  ltpnf  8472  mnflt  8474  mnfltpnf  8476  pnfnlt  8478  nltmnf  8479