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

Theorem smores2 6297
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 6290 . . . . . . 7 (Smo 𝐹 ↔ (𝐹:dom 𝐹⟢On ∧ Ord dom 𝐹 ∧ βˆ€π‘₯ ∈ dom πΉβˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯)))
21simp1bi 1012 . . . . . 6 (Smo 𝐹 β†’ 𝐹:dom 𝐹⟢On)
3 ffun 5370 . . . . . 6 (𝐹:dom 𝐹⟢On β†’ Fun 𝐹)
42, 3syl 14 . . . . 5 (Smo 𝐹 β†’ Fun 𝐹)
5 funres 5259 . . . . . 6 (Fun 𝐹 β†’ Fun (𝐹 β†Ύ 𝐴))
6 funfn 5248 . . . . . 6 (Fun (𝐹 β†Ύ 𝐴) ↔ (𝐹 β†Ύ 𝐴) Fn dom (𝐹 β†Ύ 𝐴))
75, 6sylib 122 . . . . 5 (Fun 𝐹 β†’ (𝐹 β†Ύ 𝐴) Fn dom (𝐹 β†Ύ 𝐴))
84, 7syl 14 . . . 4 (Smo 𝐹 β†’ (𝐹 β†Ύ 𝐴) Fn dom (𝐹 β†Ύ 𝐴))
9 df-ima 4641 . . . . . 6 (𝐹 β€œ 𝐴) = ran (𝐹 β†Ύ 𝐴)
10 imassrn 4983 . . . . . 6 (𝐹 β€œ 𝐴) βŠ† ran 𝐹
119, 10eqsstrri 3190 . . . . 5 ran (𝐹 β†Ύ 𝐴) βŠ† ran 𝐹
12 frn 5376 . . . . . 6 (𝐹:dom 𝐹⟢On β†’ ran 𝐹 βŠ† On)
132, 12syl 14 . . . . 5 (Smo 𝐹 β†’ ran 𝐹 βŠ† On)
1411, 13sstrid 3168 . . . 4 (Smo 𝐹 β†’ ran (𝐹 β†Ύ 𝐴) βŠ† On)
15 df-f 5222 . . . 4 ((𝐹 β†Ύ 𝐴):dom (𝐹 β†Ύ 𝐴)⟢On ↔ ((𝐹 β†Ύ 𝐴) Fn dom (𝐹 β†Ύ 𝐴) ∧ ran (𝐹 β†Ύ 𝐴) βŠ† On))
168, 14, 15sylanbrc 417 . . 3 (Smo 𝐹 β†’ (𝐹 β†Ύ 𝐴):dom (𝐹 β†Ύ 𝐴)⟢On)
1716adantr 276 . 2 ((Smo 𝐹 ∧ Ord 𝐴) β†’ (𝐹 β†Ύ 𝐴):dom (𝐹 β†Ύ 𝐴)⟢On)
18 smodm 6294 . . 3 (Smo 𝐹 β†’ Ord dom 𝐹)
19 ordin 4387 . . . . 5 ((Ord 𝐴 ∧ Ord dom 𝐹) β†’ Ord (𝐴 ∩ dom 𝐹))
20 dmres 4930 . . . . . 6 dom (𝐹 β†Ύ 𝐴) = (𝐴 ∩ dom 𝐹)
21 ordeq 4374 . . . . . 6 (dom (𝐹 β†Ύ 𝐴) = (𝐴 ∩ dom 𝐹) β†’ (Ord dom (𝐹 β†Ύ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)))
2220, 21ax-mp 5 . . . . 5 (Ord dom (𝐹 β†Ύ 𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))
2319, 22sylibr 134 . . . 4 ((Ord 𝐴 ∧ Ord dom 𝐹) β†’ Ord dom (𝐹 β†Ύ 𝐴))
2423ancoms 268 . . 3 ((Ord dom 𝐹 ∧ Ord 𝐴) β†’ Ord dom (𝐹 β†Ύ 𝐴))
2518, 24sylan 283 . 2 ((Smo 𝐹 ∧ Ord 𝐴) β†’ Ord dom (𝐹 β†Ύ 𝐴))
26 resss 4933 . . . . . 6 (𝐹 β†Ύ 𝐴) βŠ† 𝐹
27 dmss 4828 . . . . . 6 ((𝐹 β†Ύ 𝐴) βŠ† 𝐹 β†’ dom (𝐹 β†Ύ 𝐴) βŠ† dom 𝐹)
2826, 27ax-mp 5 . . . . 5 dom (𝐹 β†Ύ 𝐴) βŠ† dom 𝐹
291simp3bi 1014 . . . . 5 (Smo 𝐹 β†’ βˆ€π‘₯ ∈ dom πΉβˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯))
30 ssralv 3221 . . . . 5 (dom (𝐹 β†Ύ 𝐴) βŠ† dom 𝐹 β†’ (βˆ€π‘₯ ∈ dom πΉβˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯) β†’ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯)))
3128, 29, 30mpsyl 65 . . . 4 (Smo 𝐹 β†’ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯))
3231adantr 276 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) β†’ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯))
33 ordtr1 4390 . . . . . . . . . . 11 (Ord dom (𝐹 β†Ύ 𝐴) β†’ ((𝑦 ∈ π‘₯ ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) β†’ 𝑦 ∈ dom (𝐹 β†Ύ 𝐴)))
3425, 33syl 14 . . . . . . . . . 10 ((Smo 𝐹 ∧ Ord 𝐴) β†’ ((𝑦 ∈ π‘₯ ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) β†’ 𝑦 ∈ dom (𝐹 β†Ύ 𝐴)))
35 inss1 3357 . . . . . . . . . . . 12 (𝐴 ∩ dom 𝐹) βŠ† 𝐴
3620, 35eqsstri 3189 . . . . . . . . . . 11 dom (𝐹 β†Ύ 𝐴) βŠ† 𝐴
3736sseli 3153 . . . . . . . . . 10 (𝑦 ∈ dom (𝐹 β†Ύ 𝐴) β†’ 𝑦 ∈ 𝐴)
3834, 37syl6 33 . . . . . . . . 9 ((Smo 𝐹 ∧ Ord 𝐴) β†’ ((𝑦 ∈ π‘₯ ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) β†’ 𝑦 ∈ 𝐴))
3938expcomd 1441 . . . . . . . 8 ((Smo 𝐹 ∧ Ord 𝐴) β†’ (π‘₯ ∈ dom (𝐹 β†Ύ 𝐴) β†’ (𝑦 ∈ π‘₯ β†’ 𝑦 ∈ 𝐴)))
4039imp31 256 . . . . . . 7 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) ∧ 𝑦 ∈ π‘₯) β†’ 𝑦 ∈ 𝐴)
41 fvres 5541 . . . . . . 7 (𝑦 ∈ 𝐴 β†’ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) = (πΉβ€˜π‘¦))
4240, 41syl 14 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) ∧ 𝑦 ∈ π‘₯) β†’ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) = (πΉβ€˜π‘¦))
4336sseli 3153 . . . . . . . 8 (π‘₯ ∈ dom (𝐹 β†Ύ 𝐴) β†’ π‘₯ ∈ 𝐴)
44 fvres 5541 . . . . . . . 8 (π‘₯ ∈ 𝐴 β†’ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) = (πΉβ€˜π‘₯))
4543, 44syl 14 . . . . . . 7 (π‘₯ ∈ dom (𝐹 β†Ύ 𝐴) β†’ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) = (πΉβ€˜π‘₯))
4645ad2antlr 489 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) ∧ 𝑦 ∈ π‘₯) β†’ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) = (πΉβ€˜π‘₯))
4742, 46eleq12d 2248 . . . . 5 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) ∧ 𝑦 ∈ π‘₯) β†’ (((𝐹 β†Ύ 𝐴)β€˜π‘¦) ∈ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) ↔ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯)))
4847ralbidva 2473 . . . 4 (((Smo 𝐹 ∧ Ord 𝐴) ∧ π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)) β†’ (βˆ€π‘¦ ∈ π‘₯ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) ∈ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) ↔ βˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯)))
4948ralbidva 2473 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) β†’ (βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) ∈ ((𝐹 β†Ύ 𝐴)β€˜π‘₯) ↔ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ (πΉβ€˜π‘¦) ∈ (πΉβ€˜π‘₯)))
5032, 49mpbird 167 . 2 ((Smo 𝐹 ∧ Ord 𝐴) β†’ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) ∈ ((𝐹 β†Ύ 𝐴)β€˜π‘₯))
51 dfsmo2 6290 . 2 (Smo (𝐹 β†Ύ 𝐴) ↔ ((𝐹 β†Ύ 𝐴):dom (𝐹 β†Ύ 𝐴)⟢On ∧ Ord dom (𝐹 β†Ύ 𝐴) ∧ βˆ€π‘₯ ∈ dom (𝐹 β†Ύ 𝐴)βˆ€π‘¦ ∈ π‘₯ ((𝐹 β†Ύ 𝐴)β€˜π‘¦) ∈ ((𝐹 β†Ύ 𝐴)β€˜π‘₯)))
5217, 25, 50, 51syl3anbrc 1181 1 ((Smo 𝐹 ∧ Ord 𝐴) β†’ Smo (𝐹 β†Ύ 𝐴))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  βˆ€wral 2455   ∩ cin 3130   βŠ† wss 3131  Ord word 4364  Oncon0 4365  dom cdm 4628  ran crn 4629   β†Ύ cres 4630   β€œ cima 4631  Fun wfun 5212   Fn wfn 5213  βŸΆwf 5214  β€˜cfv 5218  Smo wsmo 6288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2741  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-tr 4104  df-iord 4368  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-fv 5226  df-smo 6289
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator