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

Theorem smores3 5938
 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 4659 . . . . . 6 dom (𝐴𝐵) = (𝐵 ∩ dom 𝐴)
2 incom 3156 . . . . . 6 (𝐵 ∩ dom 𝐴) = (dom 𝐴𝐵)
31, 2eqtri 2076 . . . . 5 dom (𝐴𝐵) = (dom 𝐴𝐵)
43eleq2i 2120 . . . 4 (𝐶 ∈ dom (𝐴𝐵) ↔ 𝐶 ∈ (dom 𝐴𝐵))
5 smores 5937 . . . 4 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ dom (𝐴𝐵)) → Smo ((𝐴𝐵) ↾ 𝐶))
64, 5sylan2br 276 . . 3 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵)) → Smo ((𝐴𝐵) ↾ 𝐶))
763adant3 935 . 2 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → Smo ((𝐴𝐵) ↾ 𝐶))
8 inss2 3185 . . . . . 6 (dom 𝐴𝐵) ⊆ 𝐵
98sseli 2968 . . . . 5 (𝐶 ∈ (dom 𝐴𝐵) → 𝐶𝐵)
10 ordelss 4143 . . . . . 6 ((Ord 𝐵𝐶𝐵) → 𝐶𝐵)
1110ancoms 259 . . . . 5 ((𝐶𝐵 ∧ Ord 𝐵) → 𝐶𝐵)
129, 11sylan 271 . . . 4 ((𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → 𝐶𝐵)
13123adant1 933 . . 3 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → 𝐶𝐵)
14 resabs1 4667 . . 3 (𝐶𝐵 → ((𝐴𝐵) ↾ 𝐶) = (𝐴𝐶))
15 smoeq 5935 . . 3 (((𝐴𝐵) ↾ 𝐶) = (𝐴𝐶) → (Smo ((𝐴𝐵) ↾ 𝐶) ↔ Smo (𝐴𝐶)))
1613, 14, 153syl 17 . 2 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → (Smo ((𝐴𝐵) ↾ 𝐶) ↔ Smo (𝐴𝐶)))
177, 16mpbid 139 1 ((Smo (𝐴𝐵) ∧ 𝐶 ∈ (dom 𝐴𝐵) ∧ Ord 𝐵) → Smo (𝐴𝐶))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102   ∧ w3a 896   = wceq 1259   ∈ wcel 1409   ∩ cin 2943   ⊆ wss 2944  Ord word 4126  dom cdm 4372   ↾ cres 4374  Smo wsmo 5930 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-v 2576  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-tr 3882  df-iord 4130  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-rn 4383  df-res 4384  df-iota 4894  df-fun 4931  df-fn 4932  df-f 4933  df-fv 4937  df-smo 5931 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator