Theorem oaordi 7247

Description: Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58. (Contributed by NM, 5-Dec-2004.)

Assertion

Ref	Expression
oaordi	|- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )

Proof of Theorem oaordi

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		onelon 5448	. . . . 5 |- ( ( B e. On /\ A e. B ) -> A e. On )
2	1	adantll 720	. . . 4 |- ( ( ( C e. On /\ B e. On ) /\ A e. B ) -> A e. On )
3		eloni 5433	. . . . . . . . 9 |- ( B e. On -> Ord B )
4		ordsucss 6645	. . . . . . . . 9 |- ( Ord B -> ( A e. B -> suc A C_ B ) )
5	3, 4	syl 17	. . . . . . . 8 |- ( B e. On -> ( A e. B -> suc A C_ B ) )
6	5	ad2antlr 733	. . . . . . 7 |- ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( A e. B -> suc A C_ B ) )
7		sucelon 6644	. . . . . . . . . 10 |- ( A e. On <-> suc A e. On )
8		oveq2 6298	. . . . . . . . . . . . . 14 |- ( x = suc A -> ( C +o x ) = ( C +o suc A ) )
9	8	sseq2d 3460	. . . . . . . . . . . . 13 |- ( x = suc A -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc A ) ) )
10	9	imbi2d 318	. . . . . . . . . . . 12 |- ( x = suc A -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o suc A ) ) ) )
11		oveq2 6298	. . . . . . . . . . . . . 14 |- ( x = y -> ( C +o x ) = ( C +o y ) )
12	11	sseq2d 3460	. . . . . . . . . . . . 13 |- ( x = y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o y ) ) )
13	12	imbi2d 318	. . . . . . . . . . . 12 |- ( x = y -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) ) )
14		oveq2 6298	. . . . . . . . . . . . . 14 |- ( x = suc y -> ( C +o x ) = ( C +o suc y ) )
15	14	sseq2d 3460	. . . . . . . . . . . . 13 |- ( x = suc y -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o suc y ) ) )
16	15	imbi2d 318	. . . . . . . . . . . 12 |- ( x = suc y -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
17		oveq2 6298	. . . . . . . . . . . . . 14 |- ( x = B -> ( C +o x ) = ( C +o B ) )
18	17	sseq2d 3460	. . . . . . . . . . . . 13 |- ( x = B -> ( ( C +o suc A ) C_ ( C +o x ) <-> ( C +o suc A ) C_ ( C +o B ) ) )
19	18	imbi2d 318	. . . . . . . . . . . 12 |- ( x = B -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) <-> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) )
20		ssid 3451	. . . . . . . . . . . . 13 |- ( C +o suc A ) C_ ( C +o suc A )
21	20	2a1i 12	. . . . . . . . . . . 12 |- ( suc A e. On -> ( C e. On -> ( C +o suc A ) C_ ( C +o suc A ) ) )
22		sssucid 5500	. . . . . . . . . . . . . . . . 17 |- ( C +o y ) C_ suc ( C +o y )
23		sstr2 3439	. . . . . . . . . . . . . . . . 17 |- ( ( C +o suc A ) C_ ( C +o y ) -> ( ( C +o y ) C_ suc ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) ) )
24	22, 23	mpi 20	. . . . . . . . . . . . . . . 16 |- ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ suc ( C +o y ) )
25		oasuc 7226	. . . . . . . . . . . . . . . . . 18 |- ( ( C e. On /\ y e. On ) -> ( C +o suc y ) = suc ( C +o y ) )
26	25	ancoms 455	. . . . . . . . . . . . . . . . 17 |- ( ( y e. On /\ C e. On ) -> ( C +o suc y ) = suc ( C +o y ) )
27	26	sseq2d 3460	. . . . . . . . . . . . . . . 16 |- ( ( y e. On /\ C e. On ) -> ( ( C +o suc A ) C_ ( C +o suc y ) <-> ( C +o suc A ) C_ suc ( C +o y ) ) )
28	24, 27	syl5ibr 225	. . . . . . . . . . . . . . 15 |- ( ( y e. On /\ C e. On ) -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) )
29	28	ex 436	. . . . . . . . . . . . . 14 |- ( y e. On -> ( C e. On -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
30	29	ad2antrr 732	. . . . . . . . . . . . 13 |- ( ( ( y e. On /\ suc A e. On ) /\ suc A C_ y ) -> ( C e. On -> ( ( C +o suc A ) C_ ( C +o y ) -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
31	30	a2d 29	. . . . . . . . . . . 12 |- ( ( ( y e. On /\ suc A e. On ) /\ suc A C_ y ) -> ( ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o suc y ) ) ) )
32		sucssel 5515	. . . . . . . . . . . . . . . . . . . 20 |- ( A e. On -> ( suc A C_ x -> A e. x ) )
33	7, 32	sylbir 217	. . . . . . . . . . . . . . . . . . 19 |- ( suc A e. On -> ( suc A C_ x -> A e. x ) )
34		limsuc 6676	. . . . . . . . . . . . . . . . . . . 20 |- ( Lim x -> ( A e. x <-> suc A e. x ) )
35	34	biimpd 211	. . . . . . . . . . . . . . . . . . 19 |- ( Lim x -> ( A e. x -> suc A e. x ) )
36	33, 35	sylan9r 664	. . . . . . . . . . . . . . . . . 18 |- ( ( Lim x /\ suc A e. On ) -> ( suc A C_ x -> suc A e. x ) )
37	36	imp 431	. . . . . . . . . . . . . . . . 17 |- ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> suc A e. x )
38		oveq2 6298	. . . . . . . . . . . . . . . . . 18 |- ( y = suc A -> ( C +o y ) = ( C +o suc A ) )
39	38	ssiun2s 4322	. . . . . . . . . . . . . . . . 17 |- ( suc A e. x -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
40	37, 39	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
41	40	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o suc A ) C_ U_ y e. x ( C +o y ) )
42		vex 3048	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
43		oalim 7234	. . . . . . . . . . . . . . . . . . 19 |- ( ( C e. On /\ ( x e. _V /\ Lim x ) ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
44	42, 43	mpanr1 689	. . . . . . . . . . . . . . . . . 18 |- ( ( C e. On /\ Lim x ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
45	44	ancoms 455	. . . . . . . . . . . . . . . . 17 |- ( ( Lim x /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
46	45	adantlr 721	. . . . . . . . . . . . . . . 16 |- ( ( ( Lim x /\ suc A e. On ) /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
47	46	adantlr 721	. . . . . . . . . . . . . . 15 |- ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o x ) = U_ y e. x ( C +o y ) )
48	41, 47	sseqtr4d 3469	. . . . . . . . . . . . . 14 |- ( ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) /\ C e. On ) -> ( C +o suc A ) C_ ( C +o x ) )
49	48	ex 436	. . . . . . . . . . . . 13 |- ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) )
50	49	a1d 26	. . . . . . . . . . . 12 |- ( ( ( Lim x /\ suc A e. On ) /\ suc A C_ x ) -> ( A. y e. x ( suc A C_ y -> ( C e. On -> ( C +o suc A ) C_ ( C +o y ) ) ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o x ) ) ) )
51	10, 13, 16, 19, 21, 31, 50	tfindsg 6687	. . . . . . . . . . 11 |- ( ( ( B e. On /\ suc A e. On ) /\ suc A C_ B ) -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) )
52	51	exp31 609	. . . . . . . . . 10 |- ( B e. On -> ( suc A e. On -> ( suc A C_ B -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
53	7, 52	syl5bi 221	. . . . . . . . 9 |- ( B e. On -> ( A e. On -> ( suc A C_ B -> ( C e. On -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
54	53	com4r 89	. . . . . . . 8 |- ( C e. On -> ( B e. On -> ( A e. On -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) ) ) )
55	54	imp31 434	. . . . . . 7 |- ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( suc A C_ B -> ( C +o suc A ) C_ ( C +o B ) ) )
56		oasuc 7226	. . . . . . . . . 10 |- ( ( C e. On /\ A e. On ) -> ( C +o suc A ) = suc ( C +o A ) )
57	56	sseq1d 3459	. . . . . . . . 9 |- ( ( C e. On /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) <-> suc ( C +o A ) C_ ( C +o B ) ) )
58		ovex 6318	. . . . . . . . . 10 |- ( C +o A ) e. _V
59		sucssel 5515	. . . . . . . . . 10 |- ( ( C +o A ) e. _V -> ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
60	58, 59	ax-mp 5	. . . . . . . . 9 |- ( suc ( C +o A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) )
61	57, 60	syl6bi 232	. . . . . . . 8 |- ( ( C e. On /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
62	61	adantlr 721	. . . . . . 7 |- ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( ( C +o suc A ) C_ ( C +o B ) -> ( C +o A ) e. ( C +o B ) ) )
63	6, 55, 62	3syld 57	. . . . . 6 |- ( ( ( C e. On /\ B e. On ) /\ A e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
64	63	imp 431	. . . . 5 |- ( ( ( ( C e. On /\ B e. On ) /\ A e. On ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
65	64	an32s 813	. . . 4 |- ( ( ( ( C e. On /\ B e. On ) /\ A e. B ) /\ A e. On ) -> ( C +o A ) e. ( C +o B ) )
66	2, 65	mpdan 674	. . 3 |- ( ( ( C e. On /\ B e. On ) /\ A e. B ) -> ( C +o A ) e. ( C +o B ) )
67	66	ex 436	. 2 |- ( ( C e. On /\ B e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )
68	67	ancoms 455	1 |- ( ( B e. On /\ C e. On ) -> ( A e. B -> ( C +o A ) e. ( C +o B ) ) )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1444   e. wcel 1887   A.wral 2737   _Vcvv 3045   C_ wss 3404   U_ciun 4278   Ord word 5422   Oncon0 5423   Lim wlim 5424   suc csuc 5425  (class class class)co 6290   +o coa 7179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-oadd 7186

This theorem is referenced by:  oaord  7248  oaass  7262  odi  7280