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

Theorem ltrenn 7627
 Description: Ordering of natural numbers with
Assertion
Ref Expression
ltrenn (𝐽 <N 𝐾 → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
Distinct variable groups:   𝐽,𝑙   𝑢,𝐽   𝐾,𝑙   𝑢,𝐾

Proof of Theorem ltrenn
StepHypRef Expression
1 ltrelpi 7096 . . 3 <N ⊆ (N × N)
21brel 4559 . 2 (𝐽 <N 𝐾 → (𝐽N𝐾N))
3 ltrennb 7626 . . 3 ((𝐽N𝐾N) → (𝐽 <N 𝐾 ↔ ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
43biimpd 143 . 2 ((𝐽N𝐾N) → (𝐽 <N 𝐾 → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩))
52, 4mpcom 36 1 (𝐽 <N 𝐾 → ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐽, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐽, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩ < ⟨[⟨(⟨{𝑙𝑙 <Q [⟨𝐾, 1o⟩] ~Q }, {𝑢 ∣ [⟨𝐾, 1o⟩] ~Q <Q 𝑢}⟩ +P 1P), 1P⟩] ~R , 0R⟩)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1463  {cab 2101  ⟨cop 3498   class class class wbr 3897  (class class class)co 5740  1oc1o 6272  [cec 6393  Ncnpi 7044
 Copyright terms: Public domain W3C validator