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

Theorem ltposr 7002
 Description: Signed real 'less than' is a partial order. (Contributed by Jim Kingdon, 4-Jan-2019.)
Assertion
Ref Expression
ltposr <R Po R

Proof of Theorem ltposr
Dummy variables 𝑥 𝑦 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-nr 6966 . . . . 5 R = ((P × P) / ~R )
2 id 19 . . . . . . 7 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → [⟨𝑥, 𝑦⟩] ~R = 𝑓)
32, 2breq12d 3806 . . . . . 6 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑥, 𝑦⟩] ~R𝑓 <R 𝑓))
43notbid 625 . . . . 5 ([⟨𝑥, 𝑦⟩] ~R = 𝑓 → (¬ [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑥, 𝑦⟩] ~R ↔ ¬ 𝑓 <R 𝑓))
5 ltsopr 6848 . . . . . . . 8 <P Or P
6 ltrelpr 6757 . . . . . . . 8 <P ⊆ (P × P)
75, 6soirri 4749 . . . . . . 7 ¬ (𝑥 +P 𝑦)<P (𝑥 +P 𝑦)
8 addcomprg 6830 . . . . . . . 8 ((𝑥P𝑦P) → (𝑥 +P 𝑦) = (𝑦 +P 𝑥))
98breq2d 3805 . . . . . . 7 ((𝑥P𝑦P) → ((𝑥 +P 𝑦)<P (𝑥 +P 𝑦) ↔ (𝑥 +P 𝑦)<P (𝑦 +P 𝑥)))
107, 9mtbii 632 . . . . . 6 ((𝑥P𝑦P) → ¬ (𝑥 +P 𝑦)<P (𝑦 +P 𝑥))
11 ltsrprg 6986 . . . . . . 7 (((𝑥P𝑦P) ∧ (𝑥P𝑦P)) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑥, 𝑦⟩] ~R ↔ (𝑥 +P 𝑦)<P (𝑦 +P 𝑥)))
1211anidms 389 . . . . . 6 ((𝑥P𝑦P) → ([⟨𝑥, 𝑦⟩] ~R <R [⟨𝑥, 𝑦⟩] ~R ↔ (𝑥 +P 𝑦)<P (𝑦 +P 𝑥)))
1310, 12mtbird 631 . . . . 5 ((𝑥P𝑦P) → ¬ [⟨𝑥, 𝑦⟩] ~R <R [⟨𝑥, 𝑦⟩] ~R )
141, 4, 13ecoptocl 6259 . . . 4 (𝑓R → ¬ 𝑓 <R 𝑓)
1514adantl 271 . . 3 ((⊤ ∧ 𝑓R) → ¬ 𝑓 <R 𝑓)
16 lttrsr 7001 . . . 4 ((𝑓R𝑔RR) → ((𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R ))
1716adantl 271 . . 3 ((⊤ ∧ (𝑓R𝑔RR)) → ((𝑓 <R 𝑔𝑔 <R ) → 𝑓 <R ))
1815, 17ispod 4067 . 2 (⊤ → <R Po R)
1918trud 1294 1 <R Po R
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103   ∧ w3a 920   = wceq 1285  ⊤wtru 1286   ∈ wcel 1434  ⟨cop 3409   class class class wbr 3793   Po wpo 4057  (class class class)co 5543  [cec 6170  Pcnp 6543   +P cpp 6545
 Copyright terms: Public domain W3C validator