Theorem ordom 3198

Description: Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43.

Assertion

Ref	Expression
ordom	|- Ord om

Proof of Theorem ordom

Step	Hyp	Ref	Expression
1		dftr2 2737	. . 3 |- (Tr om <-> A.yA.x((y e. x /\ x e. om) -> y e. om))
2		ordelord 3027	. . . . . . . 8 |- ((Ord x /\ y e. x) -> Ord y)
3		nnord 3197	. . . . . . . 8 |- (x e. om -> Ord x)
4	2, 3	sylan 459	. . . . . . 7 |- ((x e. om /\ y e. x) -> Ord y)
5	4	ancoms 447	. . . . . 6 |- ((y e. x /\ x e. om) -> Ord y)
6		trel 2742	. . . . . . . . . . . . 13 |- (Tr z -> ((y e. x /\ x e. z) -> y e. z))
7	6	exp3a 383	. . . . . . . . . . . 12 |- (Tr z -> (y e. x -> (x e. z -> y e. z)))
8	7	com12 11	. . . . . . . . . . 11 |- (y e. x -> (Tr z -> (x e. z -> y e. z)))
9		limord 3085	. . . . . . . . . . . 12 |- (Lim z -> Ord z)
10		ordtr 3019	. . . . . . . . . . . 12 |- (Ord z -> Tr z)
11	9, 10	syl 10	. . . . . . . . . . 11 |- (Lim z -> Tr z)
12	8, 11	syl5 21	. . . . . . . . . 10 |- (y e. x -> (Lim z -> (x e. z -> y e. z)))
13	12	a2d 13	. . . . . . . . 9 |- (y e. x -> ((Lim z -> x e. z) -> (Lim z -> y e. z)))
14	13	19.20dv 1331	. . . . . . . 8 |- (y e. x -> (A.z(Lim z -> x e. z) -> A.z(Lim z -> y e. z)))
15		visset 1860	. . . . . . . . . 10 |- x e. V
16	15	elom 3191	. . . . . . . . 9 |- (x e. om <-> (Ord x /\ A.z(Lim z -> x e. z)))
17	16	pm3.27bi 333	. . . . . . . 8 |- (x e. om -> A.z(Lim z -> x e. z))
18	14, 17	syl5 21	. . . . . . 7 |- (y e. x -> (x e. om -> A.z(Lim z -> y e. z)))
19	18	imp 357	. . . . . 6 |- ((y e. x /\ x e. om) -> A.z(Lim z -> y e. z))
20	5, 19	jca 295	. . . . 5 |- ((y e. x /\ x e. om) -> (Ord y /\ A.z(Lim z -> y e. z)))
21		visset 1860	. . . . . 6 |- y e. V
22	21	elom 3191	. . . . 5 |- (y e. om <-> (Ord y /\ A.z(Lim z -> y e. z)))
23	20, 22	sylibr 207	. . . 4 |- ((y e. x /\ x e. om) -> y e. om)
24	23	ax-gen 1004	. . 3 |- A.x((y e. x /\ x e. om) -> y e. om)
25	1, 24	mpgbir 1029	. 2 |- Tr om
26		omsson 3193	. 2 |- om (_ On
27		ordon 3044	. 2 |- Ord On
28		trssord 3022	. 2 |- ((Tr om /\ om (_ On /\ Ord On) -> Ord om)
29	25, 26, 27, 28	mp3an 928	1 |- Ord om

Syntax hints:   -> wi 3   /\ wa 230  A.wal 995   e. wcel 999   (_ wss 2098  Tr wtr 2735  Ord word 3004  Oncon0 3005  Lim wlim 3006  omcom 3188

This theorem is referenced by:  elnn 3199  omon 3200  limom 3203  peano5 3210  ssnlim 3224  nnarcl 4290  oaabslem 4309  oaabs 4310  onomeneq 4583  ominf 4593  omsdomnn 4594  alephgeom 4947  iscard3 4953

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-om 3189

Copyright terms: Public domain