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

Theorem smores3 6120
Description: A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
Assertion
Ref Expression
smores3 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → Smo (𝐴𝐶))

Proof of Theorem smores3
StepHypRef Expression
1 dmres 4776 . . . . . 6 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
2 incom 3215 . . . . . 6 (𝐵 ∩ dom 𝐴) = (dom 𝐴𝐵)
31, 2eqtri 2120 . . . . 5 dom (𝐴𝐵) = (dom 𝐴𝐵)
43eleq2i 2166 . . . 4 (𝐶 ∈ dom (𝐴𝐵) ↔ 𝐶 ∈ (dom 𝐴𝐵))
5 smores 6119 . . . 4 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ dom (𝐴𝐵)) → Smo ((𝐴𝐵) ↾ 𝐶))
64, 5sylan2br 284 . . 3 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵)) → Smo ((𝐴𝐵) ↾ 𝐶))
763adant3 969 . 2 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → Smo ((𝐴𝐵) ↾ 𝐶))
8 inss2 3244 . . . . . 6 (dom 𝐴𝐵) ⊆ 𝐵
98sseli 3043 . . . . 5 (𝐶 ∈ (dom 𝐴𝐵) → 𝐶𝐵)
10 ordelss 4239 . . . . . 6 ((Ord 𝐵𝐶𝐵) → 𝐶𝐵)
1110ancoms 266 . . . . 5 ((𝐶𝐵 ∧ Ord 𝐵) → 𝐶𝐵)
129, 11sylan 279 . . . 4 ((𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → 𝐶𝐵)
13123adant1 967 . . 3 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → 𝐶𝐵)
14 resabs1 4784 . . 3 (𝐶𝐵 → ((𝐴𝐵) ↾ 𝐶) = (𝐴𝐶))
15 smoeq 6117 . . 3 (((𝐴𝐵) ↾ 𝐶) = (𝐴𝐶) → (Smo ((𝐴𝐵) ↾ 𝐶) ↔ Smo (𝐴𝐶)))
1613, 14, 153syl 17 . 2 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → (Smo ((𝐴𝐵) ↾ 𝐶) ↔ Smo (𝐴𝐶)))
177, 16mpbid 146 1 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → Smo (𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  w3a 930   = wceq 1299  wcel 1448  cin 3020  wss 3021  Ord word 4222  dom cdm 4477  cres 4479  Smo wsmo 6112
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-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-rex 2381  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-tr 3967  df-iord 4226  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-rn 4488  df-res 4489  df-iota 5024  df-fun 5061  df-fn 5062  df-f 5063  df-fv 5067  df-smo 6113
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator