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

Theorem eqord1 8058
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 499 . . . . . 6 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶𝑆)
2 elisset 2647 . . . . . 6 (𝐶𝑆 → ∃𝑥 𝑥 = 𝐶)
31, 2syl 14 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ∃𝑥 𝑥 = 𝐶)
43adantr 271 . . . 4 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → ∃𝑥 𝑥 = 𝐶)
5 ltord.2 . . . . . 6 (𝑥 = 𝐶𝐴 = 𝑀)
65adantl 272 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑀)
7 eqeq2 2104 . . . . . . . 8 (𝐶 = 𝐷 → (𝑥 = 𝐶𝑥 = 𝐷))
87adantl 272 . . . . . . 7 (((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) → (𝑥 = 𝐶𝑥 = 𝐷))
98biimpa 291 . . . . . 6 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑥 = 𝐷)
10 ltord.3 . . . . . 6 (𝑥 = 𝐷𝐴 = 𝑁)
119, 10syl 14 . . . . 5 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝐴 = 𝑁)
126, 11eqtr3d 2129 . . . 4 ((((𝜑 ∧ (𝐶𝑆𝐷𝑆)) ∧ 𝐶 = 𝐷) ∧ 𝑥 = 𝐶) → 𝑀 = 𝑁)
134, 12exlimddv 1833 . . 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 8057 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝐶 < 𝐷𝑀 < 𝑁))
2019con3d 599 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑀 < 𝑁 → ¬ 𝐶 < 𝐷))
2115, 10, 5, 16, 17, 18ltordlem 8057 . . . . . 6 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (𝐷 < 𝐶𝑁 < 𝑀))
2221con3d 599 . . . . 5 ((𝜑 ∧ (𝐷𝑆𝐶𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2322ancom2s 534 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (¬ 𝑁 < 𝑀 → ¬ 𝐷 < 𝐶))
2420, 23anim12d 329 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → ((¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀) → (¬ 𝐶 < 𝐷 ∧ ¬ 𝐷 < 𝐶)))
2517ralrimiva 2458 . . . . . 6 (𝜑 → ∀𝑥𝑆 𝐴 ∈ ℝ)
265eleq1d 2163 . . . . . . 7 (𝑥 = 𝐶 → (𝐴 ∈ ℝ ↔ 𝑀 ∈ ℝ))
2726rspccva 2735 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐶𝑆) → 𝑀 ∈ ℝ)
2825, 27sylan 278 . . . . 5 ((𝜑𝐶𝑆) → 𝑀 ∈ ℝ)
2928adantrr 464 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑀 ∈ ℝ)
3010eleq1d 2163 . . . . . . 7 (𝑥 = 𝐷 → (𝐴 ∈ ℝ ↔ 𝑁 ∈ ℝ))
3130rspccva 2735 . . . . . 6 ((∀𝑥𝑆 𝐴 ∈ ℝ ∧ 𝐷𝑆) → 𝑁 ∈ ℝ)
3225, 31sylan 278 . . . . 5 ((𝜑𝐷𝑆) → 𝑁 ∈ ℝ)
3332adantrl 463 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝑁 ∈ ℝ)
3429, 33lttri3d 7696 . . 3 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → (𝑀 = 𝑁 ↔ (¬ 𝑀 < 𝑁 ∧ ¬ 𝑁 < 𝑀)))
3516, 1sseldi 3037 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐶 ∈ ℝ)
36 simprr 500 . . . . 5 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷𝑆)
3716, 36sseldi 3037 . . . 4 ((𝜑 ∧ (𝐶𝑆𝐷𝑆)) → 𝐷 ∈ ℝ)
3835, 37lttri3d 7696 . . 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 1296  wex 1433  wcel 1445  wral 2370  wss 3013   class class class wbr 3867  cr 7446   < clt 7619
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-pre-ltirr 7554  ax-pre-apti 7557
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-opab 3922  df-xp 4473  df-pnf 7621  df-mnf 7622  df-ltxr 7624
This theorem is referenced by:  eqord2  8059  reef11  11139
  Copyright terms: Public domain W3C validator