Theorem ordom 4127

Description: Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
ordom	|- Ord om

Proof of Theorem ordom

Step	Hyp	Ref	Expression
1		dftr2 3613	. . 3 |- (Tr om <-> A.yA.x((y e. x /\ x e. om) -> y e. om))
2		ordelord 3865	. . . . . . . 8 |- ((Ord x /\ y e. x) -> Ord y)
3	2	expcom 495	. . . . . . 7 |- (y e. x -> (Ord x -> Ord y))
4		limord 3901	. . . . . . . . . . . 12 |- (Lim z -> Ord z)
5		ordtr 3857	. . . . . . . . . . . 12 |- (Ord z -> Tr z)
6		trel 3618	. . . . . . . . . . . 12 |- (Tr z -> ((y e. x /\ x e. z) -> y e. z))
7	4, 5, 6	3syl 38	. . . . . . . . . . 11 |- (Lim z -> ((y e. x /\ x e. z) -> y e. z))
8	7	exp3a 496	. . . . . . . . . 10 |- (Lim z -> (y e. x -> (x e. z -> y e. z)))
9	8	com12 26	. . . . . . . . 9 |- (y e. x -> (Lim z -> (x e. z -> y e. z)))
10	9	a2d 19	. . . . . . . 8 |- (y e. x -> ((Lim z -> x e. z) -> (Lim z -> y e. z)))
11	10	alimdv 1966	. . . . . . 7 |- (y e. x -> (A.z(Lim z -> x e. z) -> A.z(Lim z -> y e. z)))
12	3, 11	anim12d 629	. . . . . 6 |- (y e. x -> ((Ord x /\ A.z(Lim z -> x e. z)) -> (Ord y /\ A.z(Lim z -> y e. z))))
13		visset 2572	. . . . . . 7 |- x e. _V
14	13	elom 4120	. . . . . 6 |- (x e. om <-> (Ord x /\ A.z(Lim z -> x e. z)))
15		visset 2572	. . . . . . 7 |- y e. _V
16	15	elom 4120	. . . . . 6 |- (y e. om <-> (Ord y /\ A.z(Lim z -> y e. z)))
17	12, 14, 16	3imtr4g 333	. . . . 5 |- (y e. x -> (x e. om -> y e. om))
18	17	imp 489	. . . 4 |- ((y e. x /\ x e. om) -> y e. om)
19	18	ax-gen 1622	. . 3 |- A.x((y e. x /\ x e. om) -> y e. om)
20	1, 19	mpgbir 1652	. 2 |- Tr om
21		omsson 4122	. 2 |- om C_ On
22		ordon 4040	. 2 |- Ord On
23		trssord 3860	. 2 |- ((Tr om /\ om C_ On /\ Ord On) -> Ord om)
24	20, 21, 22, 23	mp3an 1494	1 |- Ord om

Syntax hints:   -> wi 3   /\ wa 433  A.wal 1613   e. wcel 1617   C_ wss 2859  Tr wtr 3611  Ord word 3842  Oncon0 3843  Lim wlim 3844  omcom 4117

This theorem is referenced by:  elnn 4128  omon 4129  limom 4133  ssnlim 4136  peano5 4141  nnarcl 5490  oaabslem 5509  oaabs 5510  onomeneq 5848  ominf 5869  omsdomnn 5870  alephgeom 6229  omsublim 6243  iscard3 6283  cflim2 6350  omsublimOLD 16481

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118

Copyright terms: Public domain