Theorem oaordi 4164

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 2962	. . . . 5 |- ((B e. On /\ A e. B) -> A e. On)
2	1	adantll 392	. . . 4 |- (((C e. On /\ B e. On) /\ A e. B) -> A e. On)
3		eloni 2948	. . . . . . . . . 10 |- (B e. On -> Ord B)
4		ordsucss 3059	. . . . . . . . . 10 |- (Ord B -> (A e. B -> suc A (_ B))
5	3, 4	syl 10	. . . . . . . . 9 |- (B e. On -> (A e. B -> suc A (_ B))
6	5	ad2antlr 405	. . . . . . . 8 |- (((C e. On /\ B e. On) /\ A e. On) -> (A e. B -> suc A (_ B))
7		opreq2 3954	. . . . . . . . . . . . . . 15 |- (x = suc A -> (C +o x) = (C +o suc A))
8	7	sseq2d 2079	. . . . . . . . . . . . . 14 |- (x = suc A -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o suc A)))
9	8	imbi2d 610	. . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . 15 |- (x = y -> (C +o x) = (C +o y))
11	10	sseq2d 2079	. . . . . . . . . . . . . 14 |- (x = y -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o y)))
12	11	imbi2d 610	. . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . 15 |- (x = suc y -> (C +o x) = (C +o suc y))
14	13	sseq2d 2079	. . . . . . . . . . . . . 14 |- (x = suc y -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o suc y)))
15	14	imbi2d 610	. . . . . . . . . . . . 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 3954	. . . . . . . . . . . . . . 15 |- (x = B -> (C +o x) = (C +o B))
17	16	sseq2d 2079	. . . . . . . . . . . . . 14 |- (x = B -> ((C +o suc A) (_ (C +o x) <-> (C +o suc A) (_ (C +o B)))
18	17	imbi2d 610	. . . . . . . . . . . . 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 2070	. . . . . . . . . . . . . . 15 |- (C +o suc A) (_ (C +o suc A)
20	19	a1i 8	. . . . . . . . . . . . . 14 |- (C e. On -> (C +o suc A) (_ (C +o suc A))
21	20	a1i 8	. . . . . . . . . . . . 13 |- (suc A e. On -> (C e. On -> (C +o suc A) (_ (C +o suc A)))
22		oasuc 4147	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ y e. On) -> (C +o suc y) = suc (C +o y))
23	22	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- ((y e. On /\ C e. On) -> (C +o suc y) = suc (C +o y))
24	23	sseq2d 2079	. . . . . . . . . . . . . . . . 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 3037	. . . . . . . . . . . . . . . . . 18 |- (C +o y) (_ suc (C +o y)
26		sstr2 2061	. . . . . . . . . . . . . . . . . 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 210	. . . . . . . . . . . . . . . 16 |- ((y e. On /\ C e. On) -> ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ (C +o suc y)))
29	28	ex 373	. . . . . . . . . . . . . . 15 |- (y e. On -> (C e. On -> ((C +o suc A) (_ (C +o y) -> (C +o suc A) (_ (C +o suc y))))
30	29	ad2antrr 404	. . . . . . . . . . . . . 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 13	. . . . . . . . . . . . 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 3058	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. On <-> suc A e. On)
33		sucssel 3060	. . . . . . . . . . . . . . . . . . . . 21 |- (A e. On -> (suc A (_ x -> A e. x))
34	32, 33	sylbir 201	. . . . . . . . . . . . . . . . . . . 20 |- (suc A e. On -> (suc A (_ x -> A e. x))
35		limsuc 3110	. . . . . . . . . . . . . . . . . . . . 21 |- (Lim x -> (A e. x <-> suc A e. x))
36	35	biimpd 153	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A e. x -> suc A e. x))
37	34, 36	sylan9r 469	. . . . . . . . . . . . . . . . . . 19 |- ((Lim x /\ suc A e. On) -> (suc A (_ x -> suc A e. x))
38	37	imp 350	. . . . . . . . . . . . . . . . . 18 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> suc A e. x)
39		opreq2 3954	. . . . . . . . . . . . . . . . . . 19 |- (y = suc A -> (C +o y) = (C +o suc A))
40	39	ssiun2s 2584	. . . . . . . . . . . . . . . . . 18 |- (suc A e. x -> (C +o suc A) (_ U_y e. x (C +o y))
41	38, 40	syl 10	. . . . . . . . . . . . . . . . 17 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (C +o suc A) (_ U_y e. x (C +o y))
42	41	adantr 389	. . . . . . . . . . . . . . . 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 1804	. . . . . . . . . . . . . . . . . . . 20 |- x e. V
44		oalim 4151	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. On /\ (x e. V /\ Lim x)) -> (C +o x) = U_y e. x (C +o y))
45	43, 44	mpanr1 707	. . . . . . . . . . . . . . . . . . 19 |- ((C e. On /\ Lim x) -> (C +o x) = U_y e. x (C +o y))
46	45	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ C e. On) -> (C +o x) = U_y e. x (C +o y))
47	46	adantlr 393	. . . . . . . . . . . . . . . . 17 |- (((Lim x /\ suc A e. On) /\ C e. On) -> (C +o x) = U_y e. x (C +o y))
48	47	adantlr 393	. . . . . . . . . . . . . . . 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 2088	. . . . . . . . . . . . . . 15 |- ((((Lim x /\ suc A e. On) /\ suc A (_ x) /\ C e. On) -> (C +o suc A) (_ (C +o x))
50	49	ex 373	. . . . . . . . . . . . . 14 |- (((Lim x /\ suc A e. On) /\ suc A (_ x) -> (C e. On -> (C +o suc A) (_ (C +o x)))
51	50	a1d 12	. . . . . . . . . . . . 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 3152	. . . . . . . . . . . 12 |- (((B e. On /\ suc A e. On) /\ suc A (_ B) -> (C e. On -> (C +o suc A) (_ (C +o B)))
53	52	exp31 376	. . . . . . . . . . 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 206	. . . . . . . . . 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 362	. . . . . . . 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 4147	. . . . . . . . . 10 |- ((C e. On /\ A e. On) -> (C +o suc A) = suc (C +o A))
59	58	sseq1d 2078	. . . . . . . . 9 |- ((C e. On /\ A e. On) -> ((C +o suc A) (_ (C +o B) <-> suc (C +o A) (_ (C +o B)))
60		oprex 3968	. . . . . . . . . 10 |- (C +o A) e. V
61		sucssel 3060	. . . . . . . . . 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 7	. . . . . . . . 9 |- (suc (C +o A) (_ (C +o B) -> (C +o A) e. (C +o B))
63	59, 62	syl6bi 214	. . . . . . . 8 |- ((C e. On /\ A e. On) -> ((C +o suc A) (_ (C +o B) -> (C +o A) e. (C +o B)))
64	63	adantlr 393	. . . . . . 7 |- (((C e. On /\ B