MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  smores2 Structured version   Visualization version   GIF version

Theorem smores2 7734
Description: A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
Assertion
Ref Expression
smores2 ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹𝐴))

Proof of Theorem smores2
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfsmo2 7727 . . . . . . 7 (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
21simp1bi 1136 . . . . . 6 (Smo 𝐹𝐹:dom 𝐹⟶On)
32ffund 6295 . . . . 5 (Smo 𝐹 → Fun 𝐹)
4 funres 6177 . . . . . 6 (Fun 𝐹 → Fun (𝐹𝐴))
54funfnd 6166 . . . . 5 (Fun 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
63, 5syl 17 . . . 4 (Smo 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
7 df-ima 5368 . . . . . 6 (𝐹𝐴) = ran (𝐹𝐴)
8 imassrn 5731 . . . . . 6 (𝐹𝐴) ⊆ ran 𝐹
97, 8eqsstr3i 3855 . . . . 5 ran (𝐹𝐴) ⊆ ran 𝐹
102frnd 6298 . . . . 5 (Smo 𝐹 → ran 𝐹 ⊆ On)
119, 10syl5ss 3832 . . . 4 (Smo 𝐹 → ran (𝐹𝐴) ⊆ On)
12 df-f 6139 . . . 4 ((𝐹𝐴):dom (𝐹𝐴)⟶On ↔ ((𝐹𝐴) Fn dom (𝐹𝐴) ∧ ran (𝐹𝐴) ⊆ On))
136, 11, 12sylanbrc 578 . . 3 (Smo 𝐹 → (𝐹𝐴):dom (𝐹𝐴)⟶On)
1413adantr 474 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → (𝐹𝐴):dom (𝐹𝐴)⟶On)
15 smodm 7731 . . 3 (Smo 𝐹 → Ord dom 𝐹)
16 ordin 6006 . . . . 5 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹))
17 dmres 5668 . . . . . 6 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
18 ordeq 5983 . . . . . 6 (dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)))
1917, 18ax-mp 5 . . . . 5 (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))
2016, 19sylibr 226 . . . 4 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹𝐴))
2120ancoms 452 . . 3 ((Ord dom 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
2215, 21sylan 575 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
23 resss 5671 . . . . . 6 (𝐹𝐴) ⊆ 𝐹
24 dmss 5568 . . . . . 6 ((𝐹𝐴) ⊆ 𝐹 → dom (𝐹𝐴) ⊆ dom 𝐹)
2523, 24ax-mp 5 . . . . 5 dom (𝐹𝐴) ⊆ dom 𝐹
261simp3bi 1138 . . . . 5 (Smo 𝐹 → ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
27 ssralv 3885 . . . . 5 (dom (𝐹𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
2825, 26, 27mpsyl 68 . . . 4 (Smo 𝐹 → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
2928adantr 474 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
30 ordtr1 6019 . . . . . . . . . . 11 (Ord dom (𝐹𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
3122, 30syl 17 . . . . . . . . . 10 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
32 inss1 4053 . . . . . . . . . . . 12 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
3317, 32eqsstri 3854 . . . . . . . . . . 11 dom (𝐹𝐴) ⊆ 𝐴
3433sseli 3817 . . . . . . . . . 10 (𝑦 ∈ dom (𝐹𝐴) → 𝑦𝐴)
3531, 34syl6 35 . . . . . . . . 9 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦𝐴))
3635expcomd 408 . . . . . . . 8 ((Smo 𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹𝐴) → (𝑦𝑥𝑦𝐴)))
3736imp31 410 . . . . . . 7 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → 𝑦𝐴)
3837fvresd 6466 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
3933sseli 3817 . . . . . . . 8 (𝑥 ∈ dom (𝐹𝐴) → 𝑥𝐴)
4039fvresd 6466 . . . . . . 7 (𝑥 ∈ dom (𝐹𝐴) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4140ad2antlr 717 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4238, 41eleq12d 2853 . . . . 5 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → (((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ (𝐹𝑦) ∈ (𝐹𝑥)))
4342ralbidva 3167 . . . 4 (((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) → (∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
4443ralbidva 3167 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
4529, 44mpbird 249 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥))
46 dfsmo2 7727 . 2 (Smo (𝐹𝐴) ↔ ((𝐹𝐴):dom (𝐹𝐴)⟶On ∧ Ord dom (𝐹𝐴) ∧ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥)))
4714, 22, 45, 46syl3anbrc 1400 1 ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wral 3090  cin 3791  wss 3792  dom cdm 5355  ran crn 5356  cres 5357  cima 5358  Ord word 5975  Oncon0 5976  Fun wfun 6129   Fn wfn 6130  wf 6131  cfv 6135  Smo wsmo 7725
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-fv 6143  df-smo 7726
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator