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

Theorem smoel 5837
 Description: If x is less than y then a strictly monotone function's value will be strictly less at x than at y. (Contributed by Andrew Salmon, 22-Nov-2011.)
Assertion
Ref Expression
smoel ((Smo B A dom B 𝐶 A) → (B𝐶) (BA))

Proof of Theorem smoel
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 smodm 5828 . . . . 5 (Smo B → Ord dom B)
2 ordtr1 4074 . . . . . . 7 (Ord dom B → ((𝐶 A A dom B) → 𝐶 dom B))
32ancomsd 256 . . . . . 6 (Ord dom B → ((A dom B 𝐶 A) → 𝐶 dom B))
43expdimp 246 . . . . 5 ((Ord dom B A dom B) → (𝐶 A𝐶 dom B))
51, 4sylan 267 . . . 4 ((Smo B A dom B) → (𝐶 A𝐶 dom B))
6 df-smo 5823 . . . . . 6 (Smo B ↔ (B:dom B⟶On Ord dom B x dom By dom B(x y → (Bx) (By))))
7 eleq1 2082 . . . . . . . . . . 11 (x = 𝐶 → (x y𝐶 y))
8 fveq2 5103 . . . . . . . . . . . 12 (x = 𝐶 → (Bx) = (B𝐶))
98eleq1d 2088 . . . . . . . . . . 11 (x = 𝐶 → ((Bx) (By) ↔ (B𝐶) (By)))
107, 9imbi12d 223 . . . . . . . . . 10 (x = 𝐶 → ((x y → (Bx) (By)) ↔ (𝐶 y → (B𝐶) (By))))
11 eleq2 2083 . . . . . . . . . . 11 (y = A → (𝐶 y𝐶 A))
12 fveq2 5103 . . . . . . . . . . . 12 (y = A → (By) = (BA))
1312eleq2d 2089 . . . . . . . . . . 11 (y = A → ((B𝐶) (By) ↔ (B𝐶) (BA)))
1411, 13imbi12d 223 . . . . . . . . . 10 (y = A → ((𝐶 y → (B𝐶) (By)) ↔ (𝐶 A → (B𝐶) (BA))))
1510, 14rspc2v 2639 . . . . . . . . 9 ((𝐶 dom B A dom B) → (x dom By dom B(x y → (Bx) (By)) → (𝐶 A → (B𝐶) (BA))))
1615ancoms 255 . . . . . . . 8 ((A dom B 𝐶 dom B) → (x dom By dom B(x y → (Bx) (By)) → (𝐶 A → (B𝐶) (BA))))
1716com12 27 . . . . . . 7 (x dom By dom B(x y → (Bx) (By)) → ((A dom B 𝐶 dom B) → (𝐶 A → (B𝐶) (BA))))
18173ad2ant3 915 . . . . . 6 ((B:dom B⟶On Ord dom B x dom By dom B(x y → (Bx) (By))) → ((A dom B 𝐶 dom B) → (𝐶 A → (B𝐶) (BA))))
196, 18sylbi 114 . . . . 5 (Smo B → ((A dom B 𝐶 dom B) → (𝐶 A → (B𝐶) (BA))))
2019expdimp 246 . . . 4 ((Smo B A dom B) → (𝐶 dom B → (𝐶 A → (B𝐶) (BA))))
215, 20syld 40 . . 3 ((Smo B A dom B) → (𝐶 A → (𝐶 A → (B𝐶) (BA))))
2221pm2.43d 44 . 2 ((Smo B A dom B) → (𝐶 A → (B𝐶) (BA)))
23223impia 1087 1 ((Smo B A dom B 𝐶 A) → (B𝐶) (BA))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 873   = wceq 1228   ∈ wcel 1374  ∀wral 2284  Ord word 4048  Oncon0 4049  dom cdm 4272  ⟶wf 4825  ‘cfv 4829  Smo wsmo 5822 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004 This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-v 2537  df-un 2899  df-in 2901  df-ss 2908  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-br 3739  df-tr 3829  df-iord 4052  df-iota 4794  df-fv 4837  df-smo 5823 This theorem is referenced by:  smoiun  5838  smoel2  5840
 Copyright terms: Public domain W3C validator