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

Theorem leisorel 10520
Description: Version of isorel 5675 for strictly increasing functions on the reals. (Contributed by Mario Carneiro, 6-Apr-2015.) (Revised by Mario Carneiro, 9-Sep-2015.)
Assertion
Ref Expression
leisorel ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝐷 ↔ (𝐹𝐶) ≤ (𝐹𝐷)))

Proof of Theorem leisorel
StepHypRef Expression
1 simp1 964 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐹 Isom < , < (𝐴, 𝐵))
2 simp3r 993 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐷𝐴)
3 simp3l 992 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐶𝐴)
4 isorel 5675 . . . 4 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐷𝐴𝐶𝐴)) → (𝐷 < 𝐶 ↔ (𝐹𝐷) < (𝐹𝐶)))
54notbid 639 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐷𝐴𝐶𝐴)) → (¬ 𝐷 < 𝐶 ↔ ¬ (𝐹𝐷) < (𝐹𝐶)))
61, 2, 3, 5syl12anc 1197 . 2 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (¬ 𝐷 < 𝐶 ↔ ¬ (𝐹𝐷) < (𝐹𝐶)))
7 simp2l 990 . . . 4 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐴 ⊆ ℝ*)
87, 3sseldd 3066 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐶 ∈ ℝ*)
97, 2sseldd 3066 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐷 ∈ ℝ*)
10 xrlenlt 7793 . . 3 ((𝐶 ∈ ℝ*𝐷 ∈ ℝ*) → (𝐶𝐷 ↔ ¬ 𝐷 < 𝐶))
118, 9, 10syl2anc 406 . 2 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝐷 ↔ ¬ 𝐷 < 𝐶))
12 simp2r 991 . . . 4 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐵 ⊆ ℝ*)
13 isof1o 5674 . . . . . 6 (𝐹 Isom < , < (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
14 f1of 5333 . . . . . 6 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
151, 13, 143syl 17 . . . . 5 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → 𝐹:𝐴𝐵)
1615, 3ffvelrnd 5522 . . . 4 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐹𝐶) ∈ 𝐵)
1712, 16sseldd 3066 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐹𝐶) ∈ ℝ*)
1815, 2ffvelrnd 5522 . . . 4 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐹𝐷) ∈ 𝐵)
1912, 18sseldd 3066 . . 3 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐹𝐷) ∈ ℝ*)
20 xrlenlt 7793 . . 3 (((𝐹𝐶) ∈ ℝ* ∧ (𝐹𝐷) ∈ ℝ*) → ((𝐹𝐶) ≤ (𝐹𝐷) ↔ ¬ (𝐹𝐷) < (𝐹𝐶)))
2117, 19, 20syl2anc 406 . 2 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) ≤ (𝐹𝐷) ↔ ¬ (𝐹𝐷) < (𝐹𝐶)))
226, 11, 213bitr4d 219 1 ((𝐹 Isom < , < (𝐴, 𝐵) ∧ (𝐴 ⊆ ℝ*𝐵 ⊆ ℝ*) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝐷 ↔ (𝐹𝐶) ≤ (𝐹𝐷)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  w3a 945  wcel 1463  wss 3039   class class class wbr 3897  wf 5087  1-1-ontowf1o 5090  cfv 5091   Isom wiso 5092  *cxr 7763   < clt 7764  cle 7765
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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4014  ax-pow 4066  ax-pr 4099
This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ral 2396  df-rex 2397  df-v 2660  df-sbc 2881  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-br 3898  df-opab 3958  df-id 4183  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-f1o 5098  df-fv 5099  df-isom 5100  df-le 7770
This theorem is referenced by:  seq3coll  10525  summodclem2a  11090
  Copyright terms: Public domain W3C validator