Theorem oaabs 4236

Description: Ordinal addition absorbs a natural number added to the left of a transfinite number. Proposition 8.10 of [TakeutiZaring] p. 59.

Assertion

Ref	Expression
oaabs	|- (((A e. om /\ B e. On) /\ om (_ B) -> (A +o B) = B)

Proof of Theorem oaabs

Step	Hyp	Ref	Expression
1		ssexg 2711	. . . . . . . 8 |- ((om (_ B /\ B e. On) -> om e. V)
2	1	ex 373	. . . . . . 7 |- (om (_ B -> (B e. On -> om e. V))
3		ordom 3131	. . . . . . . 8 |- Ord om
4		elong 2946	. . . . . . . 8 |- (om e. V -> (om e. On <-> Ord om))
5	3, 4	mpbiri 194	. . . . . . 7 |- (om e. V -> om e. On)
6	2, 5	syl6com 53	. . . . . 6 |- (B e. On -> (om (_ B -> om e. On))
7	6	imp 350	. . . . 5 |- ((B e. On /\ om (_ B) -> om e. On)
8		opreq2 3954	. . . . . . . . 9 |- (x = om -> (A +o x) = (A +o om))
9		id 59	. . . . . . . . 9 |- (x = om -> x = om)
10	8, 9	eqeq12d 1481	. . . . . . . 8 |- (x = om -> ((A +o x) = x <-> (A +o om) = om))
11	10	imbi2d 610	. . . . . . 7 |- (x = om -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o om) = om)))
12		opreq2 3954	. . . . . . . . 9 |- (x = y -> (A +o x) = (A +o y))
13		id 59	. . . . . . . . 9 |- (x = y -> x = y)
14	12, 13	eqeq12d 1481	. . . . . . . 8 |- (x = y -> ((A +o x) = x <-> (A +o y) = y))
15	14	imbi2d 610	. . . . . . 7 |- (x = y -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o y) = y)))
16		opreq2 3954	. . . . . . . . 9 |- (x = suc y -> (A +o x) = (A +o suc y))
17		id 59	. . . . . . . . 9 |- (x = suc y -> x = suc y)
18	16, 17	eqeq12d 1481	. . . . . . . 8 |- (x = suc y -> ((A +o x) = x <-> (A +o suc y) = suc y))
19	18	imbi2d 610	. . . . . . 7 |- (x = suc y -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o suc y) = suc y)))
20		opreq2 3954	. . . . . . . . 9 |- (x = B -> (A +o x) = (A +o B))
21		id 59	. . . . . . . . 9 |- (x = B -> x = B)
22	20, 21	eqeq12d 1481	. . . . . . . 8 |- (x = B -> ((A +o x) = x <-> (A +o B) = B))
23	22	imbi2d 610	. . . . . . 7 |- (x = B -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o B) = B)))
24		oaabslem 4235	. . . . . . . 8 |- ((om e. On /\ A e. om) -> (A +o om) = om)
25	24	ex 373	. . . . . . 7 |- (om e. On -> (A e. om -> (A +o om) = om))
26		oasuc 4147	. . . . . . . . . . . . 13 |- ((A e. On /\ y e. On) -> (A +o suc y) = suc (A +o y))
27		nnont 3128	. . . . . . . . . . . . 13 |- (A e. om -> A e. On)
28	26, 27	sylan 448	. . . . . . . . . . . 12 |- ((A e. om /\ y e. On) -> (A +o suc y) = suc (A +o y))
29		suceq 3024	. . . . . . . . . . . 12 |- ((A +o y) = y -> suc (A +o y) = suc y)
30	28, 29	sylan9eq 1519	. . . . . . . . . . 11 |- (((A e. om /\ y e. On) /\ (A +o y) = y) -> (A +o suc y) = suc y)
31	30	exp31 376	. . . . . . . . . 10 |- (A e. om -> (y e. On -> ((A +o y) = y -> (A +o suc y) = suc y)))
32	31	com12 11	. . . . . . . . 9 |- (y e. On -> (A e. om -> ((A +o y) = y -> (A +o suc y) = suc y)))
33	32	ad2antrr 404	. . . . . . . 8 |- (((y e. On /\ om e. On) /\ om (_ y) -> (A e. om -> ((A +o y) = y -> (A +o suc y) = suc y)))
34	33	a2d 13	. . . . . . 7 |- (((y e. On /\ om e. On) /\ om (_ y) -> ((A e. om -> (A +o y) = y) -> (A e. om -> (A +o suc y) = suc y)))
35		oalim 4151	. . . . . . . . . . . . . . . . . . 19 |- ((A e. On /\ (om e. On /\ Lim om)) -> (A +o om) = U_y e. om (A +o y))
36		limom 3136	. . . . . . . . . . . . . . . . . . . 20 |- Lim om
37	36	jctr 291	. . . . . . . . . . . . . . . . . . 19 |- (om e. On -> (om e. On /\ Lim om))
38	35, 27, 37	syl2an 454	. . . . . . . . . . . . . . . . . 18 |- ((A e. om /\ om e. On) -> (A +o om) = U_y e. om (A +o y))
39	24	ancoms 436	. . . . . . . . . . . . . . . . . . 19 |- ((A e. om /\ om e. On) -> (A +o om) = om)
40		limuni 3019	. . . . . . . . . . . . . . . . . . . 20 |- (Lim om -> om = U.om)
41	36, 40	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- om = U.om
42	39, 41	syl6eq 1515	. . . . . . . . . . . . . . . . . 18 |- ((A e. om /\ om e. On) -> (A +o om) = U.om)
43	38, 42	eqtr3d 1501	. . . . . . . . . . . . . . . . 17 |- ((A e. om /\ om e. On) -> U_y e. om (A +o y) = U.om)
44	43	adantl 388	. . . . . . . . . . . . . . . 16 |- ((((Lim x /\ om (_ x) /\ A.y e. x (om (_ y -> (A +o y) = y)) /\ (A e. om /\ om e. On)) -> U_y e. om (A +o y) = U.om)
45		ordelon 2961	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Ord x /\ y e. x) -> y e. On)
46		limord 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (Lim x -> Ord x)
47	45, 46	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Lim x /\ y e. x) -> y e. On)
48		eloni 2948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. On -> Ord y)
49		ordtri1 2970	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Ord om /\ Ord y) -> (om (_ y <-> -. y e. om))
50	3, 49	mpan 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Ord y -> (om (_ y <-> -. y e. om))
51	47, 48, 50	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Lim x /\ y e. x) -> (om (_ y <-> -. y e. om))
52	51	pm5.32da 647	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (Lim x -> ((y e. x /\ om (_ y) <-> (y e. x /\ -. y e. om)))
53		eldif 2047	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. (x \ om) <-> (y e. x /\ -. y e. om))
54	52, 53	syl6bbr 536	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Lim x -> ((y e. x /\ om (_ y) <-> y e. (x \ om)))
55	54	imbi1d 611	. . . . . . . . . . . . . . . . . . . . . 22 |- (Lim x -> (((y e. x /\ om (_ y) -> (A +o y) = y) <-> (y e. (x \ om) -> (A +o y) = y)))
56		impexp 347	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. x /\ om (_ y) -> (A +o y) = y) <-> (y e. x -> (om (_ y -> (A +o y) = y)))
57	55, 56	syl5bbr 532	. . . . . . . . . . . . . . . . . . . . 21 |- (Lim x -> ((y e. x -> (om (_ y -> (A +o y) = y)) <-> (y e. (x \ om) -> (A +o y) = y)))
58	57	ralbidv2 1657	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A.y e. x (om (_ y -> (A +o y) = y) <-> A.y e. (x \ om)(A +o y) = y))
59		iuneq2 2568	. . . . . . . . . . . . . . . . . . . . 21 |- (A.y e. (x \ om)(A +o y) = y -> U_y e. (x \ om)(A +o y) = U_y e. (x \ om)y)
60		uniiun 2591	. . . . . . . . . . . . . . . . . . . . 21 |- U.(x \ om) = U_y e. (x \ om)y
61	59, 60	syl6eqr 1517	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. (x \ om)(A +o y) = y -> U_y e. (x \ om)(A +o y) = U.(x \ om))
62	58, 61	syl6bi 214	. . . . . . . . . . . . . . . . . . 19 |- (Lim x -> (A.y e. x (om (_ y -> (A +o y) = y) -> U_y e. (x \ om)(A +o y) = U.(x \ om)))
63	62	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ A.y e. x (om (_ y -> (A +o y) = y)) -> U_y e. (x \ om)(A +o y) = U.(x \ om))
64	63	adantlr 393	. . . . . . . . . . . . . . . . 17 |- (((Lim x /\ om (_ x) /\ A.y e. x (om (_ y -> (A +o y) = y)) -> U_y e. (x \ om)(A +o y) = U.(x \ om))
65	64	adantr 389	. . . . . . . . . . . . . . . 16 |- ((((Lim x /\ om (_ x) /\ A.y e. x (om (_ y -> (A +o y) = y)) /\ (A e. om /\ om e. On)) -> U_y e. (x \ om)(A +o y) = U.(x \ om))
66	44, 65	uneq12d 2175	. . . . . . . . . . . . . . 15 |- ((((Lim x /\ om (_ x) /\ A.y e. x (om (_ y -> (A +o y) = y)) /\ (A e. om /\ om e. On)) -> (U_y e. om (A +o y) u. U_y e. (x \ om)(A +o y)) = (U.om u. U.(x \ om)))
67		oalim 4151	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. On /\ (x e. V /\ Lim x)) -> (A +o x) = U_y e. x (A +o y))
68		visset 1804	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
69	68	jctl 290	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (x e. V /\ Lim x))
70	67, 27, 69	syl2an 454	. . . . . . . . . . . . . . . . . . 19 |- ((A e. om /\ Lim x) -> (A +o x) = U_y e. x (A +o y))
71	70	ancoms 436	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ A e. om) -> (A +o x) = U_y e. x (A +o y))
72		ssequn1 2190	. . . . . . . . . . . . . . . . . . . . . 22 |- (om (_ x <-> (om u. x) = x)
73	72	biimp 151	. . . . . . . . . . . . . . . . . . . . 21 |- (om (_ x -> (om u. x) = x)
74		undif2 2331	. . . . . . . . . . . . . . . . . . . . 21 |- (om u. (x \ om)) = (om u. x)
75	73, 74	syl5eq 1511	. . . . . . . . . . . . . . . . . . . 20 |- (om (_ x -> (om u. (x