Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  smoiso Unicode version

Theorem smoiso 6615
 Description: If is an isomorphism from an ordinal onto , which is a subset of the ordinals, then is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
Assertion
Ref Expression
smoiso

Proof of Theorem smoiso
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isof1o 6036 . . . 4
2 f1of 5665 . . . 4
31, 2syl 16 . . 3
4 ffdm 5596 . . . . . 6
54simpld 446 . . . . 5
6 fss 5590 . . . . 5
75, 6sylan 458 . . . 4
873adant2 976 . . 3
93, 8syl3an1 1217 . 2
10 fdm 5586 . . . . . . 7
1110eqcomd 2440 . . . . . 6
121, 2, 113syl 19 . . . . 5
13 ordeq 4580 . . . . 5
1412, 13syl 16 . . . 4
1514biimpa 471 . . 3
16153adant3 977 . 2
1710eleq2d 2502 . . . . . . 7
1810eleq2d 2502 . . . . . . 7
1917, 18anbi12d 692 . . . . . 6
201, 2, 193syl 19 . . . . 5
21 isorel 6037 . . . . . . . 8
22 epel 4489 . . . . . . . 8
23 fvex 5733 . . . . . . . . 9
2423epelc 4488 . . . . . . . 8
2521, 22, 243bitr3g 279 . . . . . . 7
2625biimpd 199 . . . . . 6
2726ex 424 . . . . 5
2820, 27sylbid 207 . . . 4
2928ralrimivv 2789 . . 3
30293ad2ant1 978 . 2
31 df-smo 6599 . 2
329, 16, 30, 31syl3anbrc 1138 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936   wceq 1652   wcel 1725  wral 2697   wss 3312   class class class wbr 4204   cep 4484   word 4572  con0 4573   cdm 4869  wf 5441  wf1o 5444  cfv 5445   wiso 5446   wsmo 6598 This theorem is referenced by:  smoiso2  6622 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-tr 4295  df-eprel 4486  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-iota 5409  df-fn 5448  df-f 5449  df-f1 5450  df-f1o 5452  df-fv 5453  df-isom 5454  df-smo 6599
 Copyright terms: Public domain W3C validator