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

Theorem smores2 5991
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 5984 . . . . . . 7 (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
21simp1bi 954 . . . . . 6 (Smo 𝐹𝐹:dom 𝐹⟶On)
3 ffun 5117 . . . . . 6 (𝐹:dom 𝐹⟶On → Fun 𝐹)
42, 3syl 14 . . . . 5 (Smo 𝐹 → Fun 𝐹)
5 funres 5008 . . . . . 6 (Fun 𝐹 → Fun (𝐹𝐴))
6 funfn 4998 . . . . . 6 (Fun (𝐹𝐴) ↔ (𝐹𝐴) Fn dom (𝐹𝐴))
75, 6sylib 120 . . . . 5 (Fun 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
84, 7syl 14 . . . 4 (Smo 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
9 df-ima 4414 . . . . . 6 (𝐹𝐴) = ran (𝐹𝐴)
10 imassrn 4740 . . . . . 6 (𝐹𝐴) ⊆ ran 𝐹
119, 10eqsstr3i 3041 . . . . 5 ran (𝐹𝐴) ⊆ ran 𝐹
12 frn 5121 . . . . . 6 (𝐹:dom 𝐹⟶On → ran 𝐹 ⊆ On)
132, 12syl 14 . . . . 5 (Smo 𝐹 → ran 𝐹 ⊆ On)
1411, 13syl5ss 3021 . . . 4 (Smo 𝐹 → ran (𝐹𝐴) ⊆ On)
15 df-f 4973 . . . 4 ((𝐹𝐴):dom (𝐹𝐴)⟶On ↔ ((𝐹𝐴) Fn dom (𝐹𝐴) ∧ ran (𝐹𝐴) ⊆ On))
168, 14, 15sylanbrc 408 . . 3 (Smo 𝐹 → (𝐹𝐴):dom (𝐹𝐴)⟶On)
1716adantr 270 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → (𝐹𝐴):dom (𝐹𝐴)⟶On)
18 smodm 5988 . . 3 (Smo 𝐹 → Ord dom 𝐹)
19 ordin 4176 . . . . 5 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord (𝐴 ∩ dom 𝐹))
20 dmres 4691 . . . . . 6 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
21 ordeq 4163 . . . . . 6 (dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹) → (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹)))
2220, 21ax-mp 7 . . . . 5 (Ord dom (𝐹𝐴) ↔ Ord (𝐴 ∩ dom 𝐹))
2319, 22sylibr 132 . . . 4 ((Ord 𝐴 ∧ Ord dom 𝐹) → Ord dom (𝐹𝐴))
2423ancoms 264 . . 3 ((Ord dom 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
2518, 24sylan 277 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → Ord dom (𝐹𝐴))
26 resss 4694 . . . . . 6 (𝐹𝐴) ⊆ 𝐹
27 dmss 4593 . . . . . 6 ((𝐹𝐴) ⊆ 𝐹 → dom (𝐹𝐴) ⊆ dom 𝐹)
2826, 27ax-mp 7 . . . . 5 dom (𝐹𝐴) ⊆ dom 𝐹
291simp3bi 956 . . . . 5 (Smo 𝐹 → ∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
30 ssralv 3069 . . . . 5 (dom (𝐹𝐴) ⊆ dom 𝐹 → (∀𝑥 ∈ dom 𝐹𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
3128, 29, 30mpsyl 64 . . . 4 (Smo 𝐹 → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
3231adantr 270 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥))
33 ordtr1 4179 . . . . . . . . . . 11 (Ord dom (𝐹𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
3425, 33syl 14 . . . . . . . . . 10 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦 ∈ dom (𝐹𝐴)))
35 inss1 3204 . . . . . . . . . . . 12 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
3620, 35eqsstri 3040 . . . . . . . . . . 11 dom (𝐹𝐴) ⊆ 𝐴
3736sseli 3006 . . . . . . . . . 10 (𝑦 ∈ dom (𝐹𝐴) → 𝑦𝐴)
3834, 37syl6 33 . . . . . . . . 9 ((Smo 𝐹 ∧ Ord 𝐴) → ((𝑦𝑥𝑥 ∈ dom (𝐹𝐴)) → 𝑦𝐴))
3938expcomd 1371 . . . . . . . 8 ((Smo 𝐹 ∧ Ord 𝐴) → (𝑥 ∈ dom (𝐹𝐴) → (𝑦𝑥𝑦𝐴)))
4039imp31 252 . . . . . . 7 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → 𝑦𝐴)
41 fvres 5274 . . . . . . 7 (𝑦𝐴 → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
4240, 41syl 14 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑦) = (𝐹𝑦))
4336sseli 3006 . . . . . . . 8 (𝑥 ∈ dom (𝐹𝐴) → 𝑥𝐴)
44 fvres 5274 . . . . . . . 8 (𝑥𝐴 → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4543, 44syl 14 . . . . . . 7 (𝑥 ∈ dom (𝐹𝐴) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4645ad2antlr 473 . . . . . 6 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
4742, 46eleq12d 2153 . . . . 5 ((((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) ∧ 𝑦𝑥) → (((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ (𝐹𝑦) ∈ (𝐹𝑥)))
4847ralbidva 2370 . . . 4 (((Smo 𝐹 ∧ Ord 𝐴) ∧ 𝑥 ∈ dom (𝐹𝐴)) → (∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
4948ralbidva 2370 . . 3 ((Smo 𝐹 ∧ Ord 𝐴) → (∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥) ↔ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 (𝐹𝑦) ∈ (𝐹𝑥)))
5032, 49mpbird 165 . 2 ((Smo 𝐹 ∧ Ord 𝐴) → ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥))
51 dfsmo2 5984 . 2 (Smo (𝐹𝐴) ↔ ((𝐹𝐴):dom (𝐹𝐴)⟶On ∧ Ord dom (𝐹𝐴) ∧ ∀𝑥 ∈ dom (𝐹𝐴)∀𝑦𝑥 ((𝐹𝐴)‘𝑦) ∈ ((𝐹𝐴)‘𝑥)))
5217, 25, 50, 51syl3anbrc 1123 1 ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  wral 2353  cin 2983  wss 2984  Ord word 4153  Oncon0 4154  dom cdm 4401  ran crn 4402  cres 4403  cima 4404  Fun wfun 4963   Fn wfn 4964  wf 4965  cfv 4969  Smo wsmo 5982
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-br 3812  df-opab 3866  df-tr 3902  df-iord 4157  df-xp 4407  df-rel 4408  df-cnv 4409  df-co 4410  df-dm 4411  df-rn 4412  df-res 4413  df-ima 4414  df-iota 4934  df-fun 4971  df-fn 4972  df-f 4973  df-fv 4977  df-smo 5983
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator