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

Theorem smores2 8394
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 8387 . . . . . . 7 (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
21simp1bi 1146 . . . . . 6 (Smo 𝐹𝐹:dom 𝐹⟶On)
32ffund 6740 . . . . 5 (Smo 𝐹 → Fun 𝐹)
4 funres 6608 . . . . . 6 (Fun 𝐹 → Fun (𝐹𝐴))
54funfnd 6597 . . . . 5 (Fun 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
63, 5syl 17 . . . 4 (Smo 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
7 df-ima 5698 . . . . . 6 (𝐹𝐴) = ran (𝐹𝐴)
8 imassrn 6089 . . . . . 6 (𝐹𝐴) ⊆ ran 𝐹
97, 8eqsstrri 4031 . . . . 5 ran (𝐹𝐴) ⊆ ran 𝐹
102frnd 6744 . . . . 5 (Smo 𝐹 → ran 𝐹 ⊆ On)
119, 10sstrid 3995 . . . 4 (Smo 𝐹 → ran (𝐹𝐴) ⊆ On)
12 df-f 6565 . . . 4 ((𝐹𝐴):dom (𝐹𝐴)⟶On ↔ ((𝐹𝐴) Fn dom (𝐹𝐴) ∧ ran (𝐹𝐴) ⊆ On))
136, 11, 12sylanbrc 583 . . 3 (Smo 𝐹 → (𝐹𝐴):dom (𝐹𝐴)⟶On)
1413adantr 480 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → (𝐹𝐴):dom (𝐹𝐴)⟶On)
15 smodm 8391 . . 3 (Smo 𝐹 → Ord dom 𝐹)
16 ordin 6414 . . . . 5 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹))
17 dmres 6030 . . . . . 6 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
18 ordeq 6391 . . . . . 6 (dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)))
1917, 18ax-mp 5 . . . . 5 (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))
2016, 19sylibr 234 . . . 4 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹𝐴))
2120ancoms 458 . . 3 ((Ord dom 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
2215, 21sylan 580 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
23 resss 6019 . . . . . 6 (𝐹𝐴) ⊆ 𝐹
24 dmss 5913 . . . . . 6 ((𝐹𝐴) ⊆ 𝐹 → dom (𝐹𝐴) ⊆ dom 𝐹)
2523, 24ax-mp 5 . . . . 5 dom (𝐹𝐴) ⊆ dom 𝐹
261simp3bi 1148 . . . . 5 (Smo 𝐹 → ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
27 ssralv 4052 . . . . 5 (dom (𝐹𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
2825, 26, 27mpsyl 68 . . . 4 (Smo 𝐹 → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
2928adantr 480 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
30 ordtr1 6427 . . . . . . . . . . 11 (Ord dom (𝐹𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
3122, 30syl 17 . . . . . . . . . 10 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
32 inss1 4237 . . . . . . . . . . . 12 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
3317, 32eqsstri 4030 . . . . . . . . . . 11 dom (𝐹𝐴) ⊆ 𝐴
3433sseli 3979 . . . . . . . . . 10 (𝑦 ∈ dom (𝐹𝐴) → 𝑦𝐴)
3531, 34syl6 35 . . . . . . . . 9 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦𝐴))
3635expcomd 416 . . . . . . . 8 ((Smo 𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹𝐴) → (𝑦𝑥𝑦𝐴)))
3736imp31 417 . . . . . . 7 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → 𝑦𝐴)
3837fvresd 6926 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
3933sseli 3979 . . . . . . . 8 (𝑥 ∈ dom (𝐹𝐴) → 𝑥𝐴)
4039fvresd 6926 . . . . . . 7 (𝑥 ∈ dom (𝐹𝐴) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4140ad2antlr 727 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4238, 41eleq12d 2835 . . . . 5 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → (((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ (𝐹𝑦) ∈ (𝐹𝑥)))
4342ralbidva 3176 . . . 4 (((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) → (∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
4443ralbidva 3176 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
4529, 44mpbird 257 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥))
46 dfsmo2 8387 . 2 (Smo (𝐹𝐴) ↔ ((𝐹𝐴):dom (𝐹𝐴)⟶On ∧ Ord dom (𝐹𝐴) ∧ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥)))
4714, 22, 45, 46syl3anbrc 1344 1 ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  wral 3061  cin 3950  wss 3951  dom cdm 5685  ran crn 5686  cres 5687  cima 5688  Ord word 6383  Oncon0 6384  Fun wfun 6555   Fn wfn 6556  wf 6557  cfv 6561  Smo wsmo 8385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2157  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-tr 5260  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-ord 6387  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569  df-smo 8386
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator