Theorem oaordi 3148

Description: Ordering property of ordinal addition. Proposition 8.4 of [TakeutiZaring] p. 58.

Assertion

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

Proof of Theorem oaordi

Step	Hyp	Ref	Expression
1		onelon 2223	. . . . 5 |- ((B e. On /\ A e. B) -> A e. On)
2	1	adantll 309	. . . 4 |- (((C e. On /\ B e. On) /\ A e. B) -> A e. On)
3		eloni 2209	. . . . . . . . . 10 |- (B e. On -> Ord B)
4		ordsucss 2320	. . . . . . . . . 10 |- (Ord B -> (A e. B -> suc A (_ B))
5	3, 4	syl 12	. . . . . . . . 9 |- (B e. On -> (A e. B -> suc A (_ B))
6	5	ad2antlr 321	. . . . . . . 8 |- (((C e. On /\ B e. On) /\ A e. On) -> (A e. B -> suc A (_ B))
7		opreq2 3007	. . . . . . . . . . . . . . 15 |- (x = suc A -> (C +o x) = (C +o suc A))
8	7	sseq2d 1528	. . . . . . . . . . . . . 14 |- (x = suc A -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o suc A)))
9	8	imbi2d 464	. . . . . . . . . . . . 13 |- (x = suc A -> ((C e. On -> (C +o suc A) (_ (C +o x)) <-> (C e. On -> (C +o suc A) (_ (C +o suc A))))
10		opreq2 3007	. . . . . . . . . . . . . . 15 |- (x = y -> (C +o x) = (C +o y))
11	10	sseq2d 1528	. . . . . . . . . . . . . 14 |- (x = y -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o y)))
12	11	imbi2d 464	. . . . . . . . . . . . 13 |- (x = y -> ((C e. On -> (C +o suc A) (_ (C +o x)) <-> (C e. On -> (C +o suc A) (_ (C +o y))))
13		opreq2 3007	. . . . . . . . . . . . . . 15 |- (x = suc y -> (C +o x) = (C +o suc y))
14	13	sseq2d 1528	. . . . . . . . . . . . . 14 |- (x = suc y -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o suc y)))
15	14	imbi2d 464	. . . . . . . . . . . . 13 |- (x = suc y -> ((C e. On -> (C +o suc A) (_ (C +o x)) <-> (C e. On -> (C +o suc A) (_ (C +o suc y))))
16		opreq2 3007	. . . . . . . . . . . . . . 15 |- (x = B -> (C +o x) = (C +o B))
17	16	sseq2d 1528	. . . . . . . . . . . . . 14 |- (x = B -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o B)))
18	17	imbi2d 464	. . . . . . . . . . . . 13 |- (x = B -> ((C e. On -> (C +o suc A) (_ (C +o x)) <-> (C e. On -> (C +o suc A) (_ (C +o B))))
19		ssid 1519	. . . . . . . . . . . . . . 15 |- (C +o suc A) (_ (C +o suc A)
20	19	a1i 7	. . . . . . . . . . . . . 14 |- (C e. On -> (C +o suc A) (_ (C +o suc A))
21	20	a1i 7	. . . . . . . . . . . . 13 |- (suc A e. On -> (C e. On -> (C +o suc A) (_ (C +o suc A)))
22		oasuc 3131	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ y e. On) -> (C +o suc y) = suc (C +o y))
23	22	ancoms 334	. . . . . . . . . . . . . . . . . 18 |- ((y e. On /\ C e. On) -> (C +o suc y) = suc (C +o y))
24	23	sseq2d 1528	. . . . . . . . . . . . . . . . 17 |- ((y e. On /\ C e. On) -> ((C +o suc A) (_ (C +o suc y) <-> (C +o suc A) (_ suc (C +o y)))
25		sssucid 2300	. . . . . . . . . . . . . . . . . 18 |- (C +o y) (_ suc (C +o y)
26		sstr2 1510	. . . . . . . . . . . . . . . . . 18 |- ((C +o suc A) (_ (C +o y) -> ((C +o y) (_ suc (C +o y) -> (C +o suc A) (_ suc (C +o y)))
27	25, 26	mpi 44	. . . . . . . . . . . . . . . . 17 |- ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ suc (C +o y))
28	24, 27	syl5bir 184	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ C e. On) -> ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ (C +o suc y)))
29	28	exp 291	. . . . . . . . . . . . . . 15 |- (y e. On -> (C e. On -> ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ (C +o suc y))))
30	29	ad2antll 320	. . . . . . . . . . . . . 14 |- (((y e. On /\ suc A e. On) /\ suc A (_ y) -> (C e. On -> ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ (C +o suc y))))
31	30	a2d 15	. . . . . . . . . . . . 13 |- (((y e. On /\ suc A e. On) /\ suc A (_ y) -> ((C e. On -> (C +o suc A) (_ (C +o y)) -> (C e. On -> (C +o suc A) (_ (C +o suc y))))
32		sucelon 2319	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. On <-> suc A e. On)
33		sucssel 2321	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. On -> (suc A (_ x -> A e. x))
34	32, 33	sylbir 176	. . . . . . . . . . . . . . . . . . . 20 |- (suc A e. On -> (suc A (_ x -> A e. x))
35		limsuc 2361	. . . . . . . . . . . . . . . . . . . . 21 |- (Lim x -> (A e. x <-> suc A e. x))
36	35	biimpd 135	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A e. x -> suc A e. x))
37	34, 36	sylan9r 360	. . . . . . . . . . . . . . . . . . 19 |- ((Lim x /\ suc A e. On) -> (suc A (_ x -> suc A e. x))
38	37	imp 277	. . . . . . . . . . . . . . . . . 18 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> suc A e. x)
39		opreq2 3007	. . . . . . . . . . . . . . . . . . 19 |- (y = suc A -> (C +o y) = (C +o suc A))
40	39	ssiun2s 2020	. . . . . . . . . . . . . . . . . 18 |- (suc A e. x -> (C +o suc A) (_ U.y e. x (C +o y))
41	38, 40	syl 12	. . . . . . . . . . . . . . . . 17 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (C +o suc A) (_ U.y e. x (C +o y))
42	41	adantr 306	. . . . . . . . . . . . . . . 16 |- ((((Lim x /\ suc A e. On) /\ suc A (_ x) /\ C e. On) -> (C +o suc A) (_ U.y e. x (C +o y))
43		visset 1350	. . . . . . . . . . . . . . . . . . . 20 |- x e. V
44		oalim 3135	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. On /\ (x e. V /\ Lim x)) -> (C +o x) = U.y e. x (C +o y))
45	43, 44	mpan21 531	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ Lim x) -> (C +o x) = U.y e. x (C +o y))
46	45	ancoms 334	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ C e. On) -> (C +o x) = U.y e. x (C +o y))
47	46	adantlr 310	. . . . . . . . . . . . . . . . 17 |- (((Lim x /\ suc A e. On) /\ C e. On) -> (C +o x) = U.y e. x (C +o y))
48	47	adantlr 310	. . . . . . . . . . . . . . . 16 |- ((((Lim x /\ suc A e. On) /\ suc A (_ x) /\ C e. On) -> (C +o x) = U.y e. x (C +o y))
49	42, 48	sseqtr4d 1537	. . . . . . . . . . . . . . 15 |- ((((Lim x /\ suc A e. On) /\ suc A (_ x) /\ C e. On) -> (C +o suc A) (_ (C +o x))
50	49	exp 291	. . . . . . . . . . . . . 14 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (C e. On -> (C +o suc A) (_ (C +o x)))
51	50	a1d 14	. . . . . . . . . . . . 13 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (A.y e. x (suc A (_ y -> (C e. On -> (C +o suc A) (_ (C +o y))) -> (C e. On -> (C +o suc A) (_ (C +o x))))
52	9, 12, 15, 18, 21, 31, 51	tfindsg 2402	. . . . . . . . . . . 12 |- (((B e. On /\ suc A e. On) /\ suc A (_ B) -> (C e. On -> (C +o suc A) (_ (C +o B)))
53	52	exp31 293	. . . . . . . . . . 11 |- (B e. On -> (suc A e. On -> (suc A (_ B -> (C e. On -> (C +o suc A) (_ (C +o B)))))
54	53, 32	syl5ib 181	. . . . . . . . . 10 |- (B e. On -> (A e. On -> (suc A (_ B -> (C e. On -> (C +o suc A) (_ (C +o B)))))
55	54	com4r 41	. . . . . . . . 9 |- (C e. On -> (B e. On -> (A e. On -> (suc A (_ B -> (C +o suc A) (_ (C +o B)))))
56	55	imp31 280	. . . . . . . 8 |- (((C e. On /\ B e. On) /\ A e. On) -> (suc A (_ B -> (C +o suc A) (_ (C +o B)))
57	6, 56	syld 27	. . . . . . 7 |- (((C e. On /\ B e. On) /\ A e. On) -> (A e. B -> (C +o suc A) (_ (C +o B)))
58		oasuc 3131	. . . . . . . . . 10 |- ((C e. On /\ A e. On) -> (C +o suc A) = suc (C +o A))
59	58	sseq1d 1527	. . . . . . . . 9 |- ((C e. On /\ A e. On) -> ((C +o suc A) (_ (C +o B) <-> suc (C +o A) (_ (C +o B)))
60		oprex 3018	. . . . . . . . . 10 |- (C +o A) e. V
61		sucssel 2321	. . . . . . . . . 10 |- ((C +o A) e. V -> (suc (C +o A) (_ (C +o B) -> (C +o A) e. (C +o B)))
62	60, 61	ax-mp 6	. . . . . . . . 9 |- (suc (C +o A) (_ (C +o B) -> (C +o A) e. (C +o B))
63	59, 62	syl6bi 187	. . . . . . . 8 |- ((C e. On /\ A e. On) -> ((C +o suc A) (_ (C +o B) -> (C +o A) e. (C +o B)))
64	63	adantlr 310	. . . . . . 7 |- (((C e. On /\ B e. On) /\ A e. On) -> ((C +o suc A) (_ (C +o B) -> (C +o A) e. (C +o B)))
65	57, 64	syld 27	. . . . . 6 |- (((C e. On /\ B e. On) /\ A e. On) -> (A e. B -> (C +o A) e. (C +o B)))
66	65	imp 277	. . .