Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltxr Structured version   GIF version

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.
StepHypRef Expression
1 breq12 3760 . . . . 5 ((x = A y = B) → (x < yA < B))
2 df-3an 886 . . . . . 6 ((x y x < y) ↔ ((x y ℝ) x < y))
32opabbii 3815 . . . . 5 {⟨x, y⟩ ∣ (x y x < y)} = {⟨x, y⟩ ∣ ((x y ℝ) x < y)}
41, 3brab2ga 4358 . . . 4 (A{⟨x, y⟩ ∣ (x y x < y)}B ↔ ((A B ℝ) A < B))
54a1i 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 ℝ))
108, 9bitri 173 . . . . . . . . . 10 (A (ℝ ∪ {-∞}) ↔ (A {-∞} A ℝ))
11 elsncg 3389 . . . . . . . . . . 11 (A * → (A {-∞} ↔ A = -∞))
1211orbi1d 704 . . . . . . . . . 10 (A * → ((A {-∞} A ℝ) ↔ (A = -∞ A ℝ)))
1310, 12syl5bb 181 . . . . . . . . 9 (A * → (A (ℝ ∪ {-∞}) ↔ (A = -∞ A ℝ)))
14 elsncg 3389 . . . . . . . . 9 (B * → (B {+∞} ↔ B = +∞))
1513, 14bi2anan9 538 . . . . . . . 8 ((A * B *) → ((A (ℝ ∪ {-∞}) B {+∞}) ↔ ((A = -∞ A ℝ) B = +∞)))
16 andir 731 . . . . . . . 8 (((A = -∞ A ℝ) B = +∞) ↔ ((A = -∞ B = +∞) (A B = +∞)))
1715, 16syl6bb 185 . . . . . . 7 ((A * B *) → ((A (ℝ ∪ {-∞}) B {+∞}) ↔ ((A = -∞ B = +∞) (A B = +∞))))
187, 17syl5bb 181 . . . . . 6 ((A * B *) → (A((ℝ ∪ {-∞}) × {+∞})B ↔ ((A = -∞ B = +∞) (A B = +∞))))
19 brxp 4318 . . . . . . 7 (A({-∞} × ℝ)B ↔ (A {-∞} B ℝ))
2011anbi1d 438 . . . . . . . 8 (A * → ((A {-∞} B ℝ) ↔ (A = -∞ B ℝ)))
2120adantr 261 . . . . . . 7 ((A * B *) → ((A {-∞} B ℝ) ↔ (A = -∞ B ℝ)))
2219, 21syl5bb 181 . . . . . 6 ((A * B *) → (A({-∞} × ℝ)B ↔ (A = -∞ B ℝ)))
2318, 22orbi12d 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 ℝ))))
2523, 24syl6bb 185 . . . 4 ((A * B *) → ((A((ℝ ∪ {-∞}) × {+∞})B A({-∞} × ℝ)B) ↔ ((A = -∞ B = +∞) ((A B = +∞) (A = -∞ B ℝ)))))
266, 25syl5bb 181 . . 3 ((A * B *) → (A(((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ))B ↔ ((A = -∞ B = +∞) ((A B = +∞) (A = -∞ B ℝ)))))
275, 26orbi12d 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)} ∪ (((ℝ ∪ {-∞}) × {+∞}) ∪ ({-∞} × ℝ)))
2928breqi 3761 . . 3 (A < BA({⟨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))
3129, 30bitri 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 ℝ)))))
3327, 31, 323bitr4g 212 1 ((A * B *) → (A < B ↔ ((((A B ℝ) A < B) (A = -∞ B = +∞)) ((A B = +∞) (A = -∞ B ℝ)))))
 Colors of variables: wff set class 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
 Copyright terms: Public domain W3C validator