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

Theorem smoiso 6192
 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 5701 . . . 4
2 f1of 5360 . . . 4
31, 2syl 14 . . 3
4 ffdm 5288 . . . . . 6
54simpld 111 . . . . 5
6 fss 5279 . . . . 5
75, 6sylan 281 . . . 4
93, 8syl3an1 1249 . 2
10 fdm 5273 . . . . . 6
1110eqcomd 2143 . . . . 5
12 ordeq 4289 . . . . 5
131, 2, 11, 124syl 18 . . . 4
1413biimpa 294 . . 3
1610eleq2d 2207 . . . . . . 7
1710eleq2d 2207 . . . . . . 7
1816, 17anbi12d 464 . . . . . 6
191, 2, 183syl 17 . . . . 5
20 epel 4209 . . . . . . . . 9
21 isorel 5702 . . . . . . . . 9
2220, 21syl5bbr 193 . . . . . . . 8
23 ffn 5267 . . . . . . . . . . 11
243, 23syl 14 . . . . . . . . . 10
2524adantr 274 . . . . . . . . 9
26 simprr 521 . . . . . . . . 9
27 funfvex 5431 . . . . . . . . . . 11
2827funfni 5218 . . . . . . . . . 10
29 epelg 4207 . . . . . . . . . 10
3028, 29syl 14 . . . . . . . . 9
3125, 26, 30syl2anc 408 . . . . . . . 8
3222, 31bitrd 187 . . . . . . 7
3332biimpd 143 . . . . . 6
3433ex 114 . . . . 5
3519, 34sylbid 149 . . . 4
3635ralrimivv 2511 . . 3