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

Theorem lteupri 6715
 Description: The difference from ltexpri 6711 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.)
Assertion
Ref Expression
lteupri (𝐴<P 𝐵 → ∃!𝑥P (𝐴 +P 𝑥) = 𝐵)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem lteupri
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 ltexpri 6711 . 2 (𝐴<P 𝐵 → ∃𝑥P (𝐴 +P 𝑥) = 𝐵)
2 ltrelpr 6603 . . . . 5 <P ⊆ (P × P)
32brel 4392 . . . 4 (𝐴<P 𝐵 → (𝐴P𝐵P))
43simpld 105 . . 3 (𝐴<P 𝐵𝐴P)
5 eqtr3 2059 . . . . . . . 8 (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → (𝐴 +P 𝑥) = (𝐴 +P 𝑦))
6 addcanprg 6714 . . . . . . . 8 ((𝐴P𝑥P𝑦P) → ((𝐴 +P 𝑥) = (𝐴 +P 𝑦) → 𝑥 = 𝑦))
75, 6syl5 28 . . . . . . 7 ((𝐴P𝑥P𝑦P) → (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → 𝑥 = 𝑦))
873expa 1104 . . . . . 6 (((𝐴P𝑥P) ∧ 𝑦P) → (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → 𝑥 = 𝑦))
98ralrimiva 2392 . . . . 5 ((𝐴P𝑥P) → ∀𝑦P (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → 𝑥 = 𝑦))
109ralrimiva 2392 . . . 4 (𝐴P → ∀𝑥P𝑦P (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → 𝑥 = 𝑦))
11 oveq2 5520 . . . . . 6 (𝑥 = 𝑦 → (𝐴 +P 𝑥) = (𝐴 +P 𝑦))
1211eqeq1d 2048 . . . . 5 (𝑥 = 𝑦 → ((𝐴 +P 𝑥) = 𝐵 ↔ (𝐴 +P 𝑦) = 𝐵))
1312rmo4 2734 . . . 4 (∃*𝑥P (𝐴 +P 𝑥) = 𝐵 ↔ ∀𝑥P𝑦P (((𝐴 +P 𝑥) = 𝐵 ∧ (𝐴 +P 𝑦) = 𝐵) → 𝑥 = 𝑦))
1410, 13sylibr 137 . . 3 (𝐴P → ∃*𝑥P (𝐴 +P 𝑥) = 𝐵)
154, 14syl 14 . 2 (𝐴<P 𝐵 → ∃*𝑥P (𝐴 +P 𝑥) = 𝐵)
16 reu5 2522 . 2 (∃!𝑥P (𝐴 +P 𝑥) = 𝐵 ↔ (∃𝑥P (𝐴 +P 𝑥) = 𝐵 ∧ ∃*𝑥P (𝐴 +P 𝑥) = 𝐵))
171, 15, 16sylanbrc 394 1 (𝐴<P 𝐵 → ∃!𝑥P (𝐴 +P 𝑥) = 𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 885   = wceq 1243   ∈ wcel 1393  ∀wral 2306  ∃wrex 2307  ∃!wreu 2308  ∃*wrmo 2309   class class class wbr 3764  (class class class)co 5512  Pcnp 6389   +P cpp 6391
 Copyright terms: Public domain W3C validator