Theorem oaabs 4310

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 2776	. . . . . . . 8 |- ((om (_ B /\ B e. On) -> om e. V)
2	1	ex 380	. . . . . . 7 |- (om (_ B -> (B e. On -> om e. V))
3		ordom 3198	. . . . . . . 8 |- Ord om
4		elong 3013	. . . . . . . 8 |- (om e. V -> (om e. On <-> Ord om))
5	3, 4	mpbiri 201	. . . . . . 7 |- (om e. V -> om e. On)
6	2, 5	syl6com 53	. . . . . 6 |- (B e. On -> (om (_ B -> om e. On))
7	6	imp 357	. . . . 5 |- ((B e. On /\ om (_ B) -> om e. On)
8		opreq2 4027	. . . . . . . . 9 |- (x = om -> (A +o x) = (A +o om))
9		id 59	. . . . . . . . 9 |- (x = om -> x = om)
10	8, 9	eqeq12d 1536	. . . . . . . 8 |- (x = om -> ((A +o x) = x <-> (A +o om) = om))
11	10	imbi2d 623	. . . . . . 7 |- (x = om -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o om) = om)))
12		opreq2 4027	. . . . . . . . 9 |- (x = y -> (A +o x) = (A +o y))
13		id 59	. . . . . . . . 9 |- (x = y -> x = y)
14	12, 13	eqeq12d 1536	. . . . . . . 8 |- (x = y -> ((A +o x) = x <-> (A +o y) = y))
15	14	imbi2d 623	. . . . . . 7 |- (x = y -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o y) = y)))
16		opreq2 4027	. . . . . . . . 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 1536	. . . . . . . 8 |- (x = suc y -> ((A +o x) = x <-> (A +o suc y) = suc y))
19	18	imbi2d 623	. . . . . . 7 |- (x = suc y -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o suc y) = suc y)))
20		opreq2 4027	. . . . . . . . 9 |- (x = B -> (A +o x) = (A +o B))
21		id 59	. . . . . . . . 9 |- (x = B -> x = B)
22	20, 21	eqeq12d 1536	. . . . . . . 8 |- (x = B -> ((A +o x) = x <-> (A +o B) = B))
23	22	imbi2d 623	. . . . . . 7 |- (x = B -> ((A e. om -> (A +o x) = x) <-> (A e. om -> (A +o B) = B)))
24		oaabslem 4309	. . . . . . . 8 |- ((om e. On /\ A e. om) -> (A +o om) = om)
25	24	ex 380	. . . . . . 7 |- (om e. On -> (A e. om -> (A +o om) = om))
26		oasuc 4221	. . . . . . . . . . . . 13 |- ((A e. On /\ y e. On) -> (A +o suc y) = suc (A +o y))
27		nnont 3195	. . . . . . . . . . . . 13 |- (A e. om -> A e. On)
28	26, 27	sylan 459	. . . . . . . . . . . 12 |- ((A e. om /\ y e. On) -> (A +o suc y) = suc (A +o y))
29		suceq 3091	. . . . . . . . . . . 12 |- ((A +o y) = y -> suc (A +o y) = suc y)
30	28, 29	sylan9eq 1574	. . . . . . . . . . 11 |- (((A e. om /\ y e. On) /\ (A +o y) = y) -> (A +o suc y) = suc y)
31	30	exp31 385	. . . . . . . . . 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 413	. . . . . . . 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 4225	. . . . . . . . . . . . . . . . . . 19 |- ((A e. On /\ (om e. On /\ Lim om)) -> (A +o om) = U_y e. om (A +o y))
36		limom 3203	. . . . . . . . . . . . . . . . . . . 20 |- Lim om
37	36	jctr 298	. . . . . . . . . . . . . . . . . . 19 |- (om e. On -> (om e. On /\ Lim om))
38	35, 27, 37	syl2an 465	. . . . . . . . . . . . . . . . . 18 |- ((A e. om /\ om e. On) -> (A +o om) = U_y e. om (A +o y))
39	24	ancoms 447	. . . . . . . . . . . . . . . . . . 19 |- ((A e. om /\ om e. On) -> (A +o om) = om)
40		limuni 3086	. . . . . . . . . . . . . . . . . . . 20 |- (Lim om -> om = U.om)
41	36, 40	ax-mp 7	. . . . . . . . . . . . . . . . . . 19 |- om = U.om
42	39, 41	syl6eq 1570	. . . . . . . . . . . . . . . . . 18 |- ((A e. om /\ om e. On) -> (A +o om) = U.om)
43	38, 42	eqtr3d 1556	. . . . . . . . . . . . . . . . 17 |- ((A e. om /\ om e. On) -> U_y e. om (A +o y) = U.om)
44	43	adantl 397	. . . . . . . . . . . . . . . 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 3028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Ord x /\ y e. x) -> y e. On)
46		limord 3085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (Lim x -> Ord x)
47	45, 46	sylan 459	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((Lim x /\ y e. x) -> y e. On)
48		eloni 3015	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y e. On -> Ord y)
49		ordtri1 3037	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((Ord om /\ Ord y) -> (om (_ y <-> -. y e. om))
50	3, 49	mpan 707	. . . . . . . . . . . . . . . . . . . . . . . . . 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 660	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (Lim x -> ((y e. x /\ om (_ y) <-> (y e. x /\ -. y e. om)))
53		eldif 2108	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. (x \ om) <-> (y e. x /\ -. y e. om))
54	52, 53	syl6bbr 549	. . . . . . . . . . . . . . . . . . . . . . 23 |- (Lim x -> ((y e. x /\ om (_ y) <-> y e. (x \ om)))
55	54	imbi1d 624	. . . . . . . . . . . . . . . . . . . . . 22 |- (Lim x -> (((y e. x /\ om (_ y) -> (A +o y) = y) <-> (y e. (x \ om) -> (A +o y) = y)))
56		impexp 354	. . . . . . . . . . . . . . . . . . . . . 22 |- (((y e. x /\ om (_ y) -> (A +o y) = y) <-> (y e. x -> (om (_ y -> (A +o y) = y)))
57	55, 56	syl5bbr 545	. . . . . . . . . . . . . . . . . . . . 21 |- (Lim x -> ((y e. x -> (om (_ y -> (A +o y) = y)) <-> (y e. (x \ om) -> (A +o y) = y)))
58	57	ralbidv2 1712	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (A.y e. x (om (_ y -> (A +o y) = y) <-> A.y e. (x \ om)(A +o y) = y))
59		iuneq2 2632	. . . . . . . . . . . . . . . . . . . . 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 2655	. . . . . . . . . . . . . . . . . . . . 21 |- U.(x \ om) = U_y e. (x \ om)y
61	59, 60	syl6eqr 1572	. . . . . . . . . . . . . . . . . . . 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 221	. . . . . . . . . . . . . . . . . . 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 357	. . . . . . . . . . . . . . . . . 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 402	. . . . . . . . . . . . . . . . 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 398	. . . . . . . . . . . . . . . 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 2236	. . . . . . . . . . . . . . 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 4225	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. On /\ (x e. V /\ Lim x)) -> (A +o x) = U_y e. x (A +o y))
68		visset 1860	. . . . . . . . . . . . . . . . . . . . 21 |- x e. V
69	68	jctl 297	. . . . . . . . . . . . . . . . . . . 20 |- (Lim x -> (x e. V /\ Lim x))
70	67, 27, 69	syl2an 465	. . . . . . . . . . . . . . . . . . 19 |- ((A e. om /\ Lim x) -> (A +o x) = U_y e. x (A +o y))
71	70	ancoms 447	. . . . . . . . . . . . . . . . . 18 |- ((Lim x /\ A e. om) -> (A +o x) = U_y e. x (A +o y))
72		ssequn1 2251	. . . . . . . . . . . . . . . . . . . . . 22 |- (om (_ x <-> (om u. x) = x)
73	72	biimpi 158	. . . . . . . . . . . . . . . . . . . . 21 |- (om (_ x -> (om u. x) = x)
74		undif2 2393	. . . . . . . . . . . . . . . . . . . . 21 |- (om u. (x \ om)) = (om u. x)
75	73, 74	syl5eq 1566	. . . . . . . . . . . . . . . . . . . 20 |- (om (_ x -> (om u. (