Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  celsor Unicode version

Theorem celsor 25111
 Description: If all the elements of a set are ordinal numbers and are parts of the set then is an ordinal number. (Contributed by FL, 20-Apr-2011.)
Assertion
Ref Expression
celsor
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem celsor
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 r19.26 2675 . . . 4
2 dftr3 4117 . . . . . . 7
32biimpri 197 . . . . . 6
4 eleq1 2343 . . . . . . . . 9
54cbvralv 2764 . . . . . . . 8
6 raaanv 3562 . . . . . . . . . 10
7 eloni 4402 . . . . . . . . . . . . 13
8 eloni 4402 . . . . . . . . . . . . 13
9 ordtri3or 4424 . . . . . . . . . . . . 13
107, 8, 9syl2an 463 . . . . . . . . . . . 12
1110ralimi 2618 . . . . . . . . . . 11
1211ralimi 2618 . . . . . . . . . 10
136, 12sylbir 204 . . . . . . . . 9
1413expcom 424 . . . . . . . 8
155, 14sylbi 187 . . . . . . 7
1615pm2.43i 43 . . . . . 6
173, 16anim12i 549 . . . . 5
1817ancoms 439 . . . 4
191, 18sylbi 187 . . 3