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

Theorem eqord1 8457
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 529 . . . . . 6 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶𝑆)
2 elisset 2765 . . . . . 6 (𝐶𝑆 → ∃𝑥 𝑥 = 𝐶)
31, 2syl 14 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ∃𝑥 𝑥 = 𝐶)
43adantr 276 . . . 4 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → ∃𝑥 𝑥 = 𝐶)
5 ltord.2 . . . . . 6 (𝑥 = 𝐶𝐴 = 𝑀)
65adantl 277 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑀)
7 eqeq2 2198 . . . . . . . 8 (𝐶 = 𝐷 → (𝑥 = 𝐶𝑥 = 𝐷))
87adantl 277 . . . . . . 7 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → (𝑥 = 𝐶𝑥 = 𝐷))
98biimpa 296 . . . . . 6 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑥 = 𝐷)
10 ltord.3 . . . . . 6 (𝑥 = 𝐷𝐴 = 𝑁)
119, 10syl 14 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑁)
126, 11eqtr3d 2223 . . . 4 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑀 = 𝑁)
134, 12exlimddv 1909 . . 3 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → 𝑀 = 𝑁)
1413ex 115 . 2 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷𝑀 = 𝑁))
15 ltord.1 . . . . . 6 (𝑥 = 𝑦𝐴 = 𝐵)
16 ltord.4 . . . . . 6 𝑆 ⊆ ℝ
17 ltord.5 . . . . . 6 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
18 ltord.6 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥 < 𝑦𝐴 < 𝐵))
1915, 5, 10, 16, 17, 18ltordlem 8456 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 < 𝐷𝑀 < 𝑁))
2019con3d 632 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑀 < 𝑁 → ¬ 𝐶 < 𝐷))
2115, 10, 5, 16, 17, 18ltordlem 8456 . . . . . 6 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (𝐷 < 𝐶𝑁 < 𝑀))
2221con3d 632 . . . . 5 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2322ancom2s 566 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2420, 23anim12d 335 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ((¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀) → (¬ 𝐶 < 𝐷 ∧ ¬ 𝐷 < 𝐶)))
2517ralrimiva 2562 . . . . . 6 (𝜑 → ∀𝑥𝑆 𝐴 ∈ ℝ)
265eleq1d 2257 . . . . . . 7 (𝑥 = 𝐶 → (𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ))
2726rspccva 2854 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐶𝑆) → 𝑀 ∈ ℝ)
2825, 27sylan 283 . . . . 5 ((𝜑𝐶𝑆) → 𝑀 ∈ ℝ)
2928adantrr 479 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑀 ∈ ℝ)
3010eleq1d 2257 . . . . . . 7 (𝑥 = 𝐷 → (𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ))
3130rspccva 2854 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐷𝑆) → 𝑁 ∈ ℝ)
3225, 31sylan 283 . . . . 5 ((𝜑𝐷𝑆) → 𝑁 ∈ ℝ)
3332adantrl 478 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑁 ∈ ℝ)
3429, 33lttri3d 8089 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝑀 = 𝑁 ↔ (¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀)))
3516, 1sselid 3167 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶 ∈ ℝ)
36 simprr 531 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷𝑆)
3716, 36sselid 3167 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷 ∈ ℝ)
3835, 37lttri3d 8089 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷 ↔ (¬ 𝐶 < 𝐷 ∧ ¬ 𝐷 < 𝐶)))
3924, 34, 383imtr4d 203 . 2 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝑀 = 𝑁𝐶 = 𝐷))
4014, 39impbid 129 1 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 = 𝐷𝑀 = 𝑁))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105   = wceq 1363  wex 1502  wcel 2159  wral 2467  wss 3143   class class class wbr 4017  cr 7827   < clt 8009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2161  ax-14 2162  ax-ext 2170  ax-sep 4135  ax-pow 4188  ax-pr 4223  ax-un 4447  ax-setind 4550  ax-cnex 7919  ax-resscn 7920  ax-pre-ltirr 7940  ax-pre-apti 7943
This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2040  df-mo 2041  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ne 2360  df-nel 2455  df-ral 2472  df-rex 2473  df-rab 2476  df-v 2753  df-dif 3145  df-un 3147  df-in 3149  df-ss 3156  df-pw 3591  df-sn 3612  df-pr 3613  df-op 3615  df-uni 3824  df-br 4018  df-opab 4079  df-xp 4646  df-pnf 8011  df-mnf 8012  df-ltxr 8014
This theorem is referenced by:  eqord2  8458  reef11  11724  nninfdclemf1  12470
  Copyright terms: Public domain W3C validator