Metamath Proof Explorer


Theorem smoiso

Description: If F is an isomorphism from an ordinal A onto B , which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 24-Nov-2011)

Ref Expression
Assertion smoiso FIsomE,EABOrdABOnSmoF

Proof

Step Hyp Ref Expression
1 isof1o FIsomE,EABF:A1-1 ontoB
2 f1of F:A1-1 ontoBF:AB
3 1 2 syl FIsomE,EABF:AB
4 ffdm F:ABF:domFBdomFA
5 4 simpld F:ABF:domFB
6 fss F:domFBBOnF:domFOn
7 5 6 sylan F:ABBOnF:domFOn
8 7 3adant2 F:ABOrdABOnF:domFOn
9 3 8 syl3an1 FIsomE,EABOrdABOnF:domFOn
10 fdm F:ABdomF=A
11 10 eqcomd F:ABA=domF
12 ordeq A=domFOrdAOrddomF
13 1 2 11 12 4syl FIsomE,EABOrdAOrddomF
14 13 biimpa FIsomE,EABOrdAOrddomF
15 14 3adant3 FIsomE,EABOrdABOnOrddomF
16 10 eleq2d F:ABxdomFxA
17 10 eleq2d F:ABydomFyA
18 16 17 anbi12d F:ABxdomFydomFxAyA
19 1 2 18 3syl FIsomE,EABxdomFydomFxAyA
20 isorel FIsomE,EABxAyAxEyFxEFy
21 epel xEyxy
22 fvex FyV
23 22 epeli FxEFyFxFy
24 20 21 23 3bitr3g FIsomE,EABxAyAxyFxFy
25 24 biimpd FIsomE,EABxAyAxyFxFy
26 25 ex FIsomE,EABxAyAxyFxFy
27 19 26 sylbid FIsomE,EABxdomFydomFxyFxFy
28 27 ralrimivv FIsomE,EABxdomFydomFxyFxFy
29 28 3ad2ant1 FIsomE,EABOrdABOnxdomFydomFxyFxFy
30 df-smo SmoFF:domFOnOrddomFxdomFydomFxyFxFy
31 9 15 29 30 syl3anbrc FIsomE,EABOrdABOnSmoF