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

Theorem eqord1 8257
Description: A strictly increasing real function on a subset of is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.)
Hypotheses
Ref Expression
ltord.1 (𝑥 = 𝑦𝐴 = 𝐵)
ltord.2 (𝑥 = 𝐶𝐴 = 𝑀)
ltord.3 (𝑥 = 𝐷𝐴 = 𝑁)
ltord.4 𝑆 ⊆ ℝ
ltord.5 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
ltord.6 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 < 𝑦𝐴 < 𝐵))
Assertion
Ref Expression
eqord1 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷𝑀 = 𝑁))
Distinct variable groups:   𝑥,𝐵   𝑥,𝑦,𝐶   𝑥,𝐷,𝑦   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑦)

Proof of Theorem eqord1
StepHypRef Expression
1 simprl 520 . . . . . 6 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶𝑆)
2 elisset 2700 . . . . . 6 (𝐶𝑆 → ∃𝑥 𝑥 = 𝐶)
31, 2syl 14 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ∃𝑥 𝑥 = 𝐶)
43adantr 274 . . . 4 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → ∃𝑥 𝑥 = 𝐶)
5 ltord.2 . . . . . 6 (𝑥 = 𝐶𝐴 = 𝑀)
65adantl 275 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑀)
7 eqeq2 2149 . . . . . . . 8 (𝐶 = 𝐷 → (𝑥 = 𝐶𝑥 = 𝐷))
87adantl 275 . . . . . . 7 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → (𝑥 = 𝐶𝑥 = 𝐷))
98biimpa 294 . . . . . 6 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑥 = 𝐷)
10 ltord.3 . . . . . 6 (𝑥 = 𝐷𝐴 = 𝑁)
119, 10syl 14 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑁)
126, 11eqtr3d 2174 . . . 4 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑀 = 𝑁)
134, 12exlimddv 1870 . . 3 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → 𝑀 = 𝑁)
1413ex 114 . 2 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷𝑀 = 𝑁))
15 ltord.1 . . . . . 6 (𝑥 = 𝑦𝐴 = 𝐵)
16 ltord.4 . . . . . 6 𝑆 ⊆ ℝ
17 ltord.5 . . . . . 6 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
18 ltord.6 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 < 𝑦𝐴 < 𝐵))
1915, 5, 10, 16, 17, 18ltordlem 8256 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 < 𝐷𝑀 < 𝑁))
2019con3d 620 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑀 < 𝑁 → ¬ 𝐶 < 𝐷))
2115, 10, 5, 16, 17, 18ltordlem 8256 . . . . . 6 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (𝐷 < 𝐶𝑁 < 𝑀))
2221con3d 620 . . . . 5 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2322ancom2s 555 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2420, 23anim12d 333 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ((¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀) → (¬ 𝐶 < 𝐷 ∧ ¬ 𝐷 < 𝐶)))
2517ralrimiva 2505 . . . . . 6 (𝜑 → ∀𝑥𝑆 𝐴 ∈ ℝ)
265eleq1d 2208 . . . . . . 7 (𝑥 = 𝐶 → (𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ))
2726rspccva 2788 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐶𝑆) → 𝑀 ∈ ℝ)
2825, 27sylan 281 . . . . 5 ((𝜑𝐶𝑆) → 𝑀 ∈ ℝ)
2928adantrr 470 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑀 ∈ ℝ)
3010eleq1d 2208 . . . . . . 7 (𝑥 = 𝐷 → (𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ))
3130rspccva 2788 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐷𝑆) → 𝑁 ∈ ℝ)
3225, 31sylan 281 . . . . 5 ((𝜑𝐷𝑆) → 𝑁 ∈ ℝ)
3332adantrl 469 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑁 ∈ ℝ)
3429, 33lttri3d 7890 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝑀 = 𝑁 ↔ (¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀)))
3516, 1sseldi 3095 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶 ∈ ℝ)
36 simprr 521 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷𝑆)
3716, 36sseldi 3095 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷 ∈ ℝ)
3835, 37lttri3d 7890 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷 ↔ (¬ 𝐶 < 𝐷 ∧ ¬ 𝐷 < 𝐶)))
3924, 34, 383imtr4d 202 . 2 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝑀 = 𝑁𝐶 = 𝐷))
4014, 39impbid 128 1 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷𝑀 = 𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104   = wceq 1331  wex 1468  wcel 1480  wral 2416  wss 3071   class class class wbr 3929  cr 7631   < clt 7812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-cnex 7723  ax-resscn 7724  ax-pre-ltirr 7744  ax-pre-apti 7747
This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-opab 3990  df-xp 4545  df-pnf 7814  df-mnf 7815  df-ltxr 7817
This theorem is referenced by:  eqord2  8258  reef11  11417
  Copyright terms: Public domain W3C validator