Theorem oawordeulem 4246

Description: Lemma for oawordex 4249.

Hypotheses

Ref	Expression
oawordeulem.1	|- A e. On
oawordeulem.2	|- B e. On
oawordeulem.3	|- S = {y e. On | B (_ (A +o y)}

Assertion

Ref	Expression
oawordeulem	|- (A (_ B -> E!x e. On (A +o x) = B)

Distinct variable groups:   x,y,A   x,B,y   x,S

Proof of Theorem oawordeulem

Step	Hyp	Ref	Expression
1		oawordeulem.3	. . . . . . . . . . 11 |- S = {y e. On | B (_ (A +o y)}
2		ssrab2 2182	. . . . . . . . . . 11 |- {y e. On | B (_ (A +o y)} (_ On
3	1, 2	eqsstri 2142	. . . . . . . . . 10 |- S (_ On
4		opreq2 4027	. . . . . . . . . . . . . 14 |- (y = B -> (A +o y) = (A +o B))
5	4	sseq2d 2140	. . . . . . . . . . . . 13 |- (y = B -> (B (_ (A +o y) <-> B (_ (A +o B)))
6	5, 1	elrab2 1954	. . . . . . . . . . . 12 |- (B e. S <-> (B e. On /\ B (_ (A +o B)))
7		oawordeulem.2	. . . . . . . . . . . 12 |- B e. On
8		oawordeulem.1	. . . . . . . . . . . . 13 |- A e. On
9		oaword2 4245	. . . . . . . . . . . . 13 |- ((B e. On /\ A e. On) -> B (_ (A +o B))
10	7, 8, 9	mp2an 709	. . . . . . . . . . . 12 |- B (_ (A +o B)
11	6, 7, 10	mpbir2an 742	. . . . . . . . . . 11 |- B e. S
12		ne0i 2337	. . . . . . . . . . 11 |- (B e. S -> S =/= (/))
13	11, 12	ax-mp 7	. . . . . . . . . 10 |- S =/= (/)
14		oninton 3069	. . . . . . . . . 10 |- ((S (_ On /\ S =/= (/)) -> |^|S e. On)
15	3, 13, 14	mp2an 709	. . . . . . . . 9 |- |^|S e. On
16		onzsl 3174	. . . . . . . . 9 |- (|^|S e. On <-> (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S)))
17	15, 16	mpbi 196	. . . . . . . 8 |- (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S))
18		opreq2 4027	. . . . . . . . . . . 12 |- (|^|S = (/) -> (A +o |^|S) = (A +o (/)))
19		oa0 4213	. . . . . . . . . . . . 13 |- (A e. On -> (A +o (/)) = A)
20	8, 19	ax-mp 7	. . . . . . . . . . . 12 |- (A +o (/)) = A
21	18, 20	syl6eq 1570	. . . . . . . . . . 11 |- (|^|S = (/) -> (A +o |^|S) = A)
22	21	sseq1d 2139	. . . . . . . . . 10 |- (|^|S = (/) -> ((A +o |^|S) (_ B <-> A (_ B))
23	22	biimprd 161	. . . . . . . . 9 |- (|^|S = (/) -> (A (_ B -> (A +o |^|S) (_ B))
24		opreq2 4027	. . . . . . . . . . . . 13 |- (|^|S = suc z -> (A +o |^|S) = (A +o suc z))
25		oasuc 4221	. . . . . . . . . . . . . 14 |- ((A e. On /\ z e. On) -> (A +o suc z) = suc (A +o z))
26	8, 25	mpan 707	. . . . . . . . . . . . 13 |- (z e. On -> (A +o suc z) = suc (A +o z))
27	24, 26	sylan9eqr 1576	. . . . . . . . . . . 12 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) = suc (A +o z))
28		visset 1860	. . . . . . . . . . . . . . . 16 |- z e. V
29	28	sucid 3108	. . . . . . . . . . . . . . 15 |- z e. suc z
30		eleq2 1582	. . . . . . . . . . . . . . 15 |- (|^|S = suc z -> (z e. |^|S <-> z e. suc z))
31	29, 30	mpbiri 201	. . . . . . . . . . . . . 14 |- (|^|S = suc z -> z e. |^|S)
32	15	oneli 3155	. . . . . . . . . . . . . . 15 |- (z e. |^|S -> z e. On)
33		opreq2 4027	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (A +o y) = (A +o z))
34	33	sseq2d 2140	. . . . . . . . . . . . . . . . . 18 |- (y = z -> (B (_ (A +o y) <-> B (_ (A +o z)))
35	34	onnminsb 3073	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (z e. |^|{y e. On | B (_ (A +o y)} -> -. B (_ (A +o z)))
36	1	inteqi 2591	. . . . . . . . . . . . . . . . . 18 |- |^|S = |^|{y e. On | B (_ (A +o y)}
37	36	eleq2i 1585	. . . . . . . . . . . . . . . . 17 |- (z e. |^|S <-> z e. |^|{y e. On | B (_ (A +o y)})
38	35, 37	syl5ib 213	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z e. |^|S -> -. B (_ (A +o z)))
39		oacl 4228	. . . . . . . . . . . . . . . . . . 19 |- ((A e. On /\ z e. On) -> (A +o z) e. On)
40	8, 39	mpan 707	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> (A +o z) e. On)
41		ontri1 3038	. . . . . . . . . . . . . . . . . . 19 |- ((B e. On /\ (A +o z) e. On) -> (B (_ (A +o z) <-> -. (A +o z) e. B))
42	7, 41	mpan 707	. . . . . . . . . . . . . . . . . 18 |- ((A +o z) e. On -> (B (_ (A +o z) <-> -. (A +o z) e. B))
43	40, 42	syl 10	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (B (_ (A +o z) <-> -. (A +o z) e. B))
44	43	con2bid 537	. . . . . . . . . . . . . . . 16 |- (z e. On -> ((A +o z) e. B <-> -. B (_ (A +o z)))
45	38, 44	sylibrd 211	. . . . . . . . . . . . . . 15 |- (z e. On -> (z e. |^|S -> (A +o z) e. B))
46	32, 45	mpcom 49	. . . . . . . . . . . . . 14 |- (z e. |^|S -> (A +o z) e. B)
47	7	onordi 3152	. . . . . . . . . . . . . . 15 |- Ord B
48		ordsucss 3126	. . . . . . . . . . . . . . 15 |- (Ord B -> ((A +o z) e. B -> suc (A +o z) (_ B))
49	47, 48	ax-mp 7	. . . . . . . . . . . . . 14 |- ((A +o z) e. B -> suc (A +o z) (_ B)
50	31, 46, 49	3syl 20	. . . . . . . . . . . . 13 |- (|^|S = suc z -> suc (A +o z) (_ B)
51	50	adantl 397	. . . . . . . . . . . 12 |- ((z e. On /\ |^|S = suc z) -> suc (A +o z) (_ B)
52	27, 51	eqsstrd 2146	. . . . . . . . . . 11 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) (_ B)
53	52	r19.23aiva 1791	. . . . . . . . . 10 |- (E.z e. On |^|S = suc z -> (A +o |^|S) (_ B)
54	53	a1d 12	. . . . . . . . 9 |- (E.z e. On |^|S = suc z -> (A (_ B -> (A +o |^|S) (_ B))
55		iunss 2645	. . . . . . . . . . . 12 |- (U_z e. |^|S(A +o z) (_ B <-> A.z e. |^|S(A +o z) (_ B)
56	7	onelssi 3157	. . . . . . . . . . . . 13 |- ((A +o z) e. B -> (A +o z) (_ B)
57	46, 56	syl 10	. . . . . . . . . . . 12 |- (z e. |^|S -> (A +o z) (_ B)
58	55, 57	mprgbir 1748	. . . . . . . . . . 11 |- U_z e. |^|S(A +o z) (_ B
59		oalim 4225	. . . . . . . . . . . . 13 |- ((A e. On /\ (|^|S e. V /\ Lim |^|S)) -> (A +o |^|S) = U_z e. |^|S(A +o z))
60	8, 59	mpan 707	. . . . . . . . . . . 12 |- ((|^|S e. V /\ Lim |^|S) -> (A +o |^|S) = U_z e. |^|S(A +o z))
61	60	sseq1d 2139	. . . . . . . . . . 11 |- ((|^|S e. V /\ Lim |^|S) -> ((A +o |^|S) (_ B <-> U_z e. |^|S(A +o z) (_ B))
62	58, 61	mpbiri 201	. . . . . . . . . 10 |- ((|^|S e. V /\ Lim |^|S) -> (A +o |^|S) (_ B)
63	62	a1d 12	. . . . . . . . 9 |- ((|^|S e. V /\ Lim |^|S) -> (A (_ B -> (A +o |^|S) (_ B))
64	23, 54, 63	3jaoi 899	. . . . . . . 8 |- ((|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S)) -> (A (_ B -> (A +o |^|S) (_ B))
65	17, 64	ax-mp 7	. . . . . . 7 |- (A (_ B -> (A +o |^|S) (_ B)
66	5	rcla4ev 1924	. . . . . . . . . 10 |- ((B e. On /\ B (_ (A +o B)) -> E.y e. On B (_ (A +o y))
67	7, 10, 66	mp2an 709	. . . . . . . . 9 |- E.y e. On B (_ (A +o y)
68		ax-17 1012	. . . . . . . . . . 11 |- (z e. B -> A.y z e. B)
69		ax-17 1012	. . . . . . . . . . . 12 |- (z e. A -> A.y z e. A)
70		ax-17 1012	. . . . . . . . . . . 12 |- (z e. +o -> A.y z e. +o )
71		hbrab1 1819	. . . . . . . . . . . . 13 |- (z e. {y e. On | B (_ (A +o y)} -> A.y z e. {y e. On | B (_ (A +o y)})
72	71	hbint 2597	. . . . . . . . . . . 12 |- (z e. |^|{y e. On | B (_ (A +o y)} -> A.y z e. |^|{y e. On | B (_ (A +o y)})
73	69, 70, 72	hbopr 4039	. . . . . . . . . . 11 |- (z e. (A +o |^|{y e. On | B (_ (A +o y)}) -> A.y z e. (A +o |^|{y e. On | B (_ (A +o y)}))
74	68, 73	hbss 2113	. . . . . . . . . 10 |- (B (_ (A +o |^|{y e. On | B (_ (A +o y)}) -> A.y B (_ (A +o |^|{y e. On | B (_ (A +o y)}))
75		opreq2 4027	. . . . . . . . . . 11 |- (y = |^|{y e. On | B (_ (A +o y)} -> (A +o y) = (A +o |^|{y e. On | B (_ (A +o y)}))
76	75	sseq2d 2140	. . . . . . . . . 10 |- (y = |^|{y e. On | B (_ (A +o y)} -> (B (_ (A +o y) <-> B (_ (A +o |^|{y e. On | B (_ (A +o y)})))
77	74, 76	onminsb 3066	. . . . . . . . 9 |- (E.y e. On B (_ (A +o y) -> B (_ (A +o |^|{y e. On | B (_ (A +o y)}))
78	67, 77	ax-mp 7	. . . . . . . 8 |- B (_ (A +o |^|{y e. On | B (_ (A +o y)})
79	36	opreq2i 4030	. . . . . . . 8 |- (A +o |^|S) = (A +o |^|{y e. On | B (_ (A +o y)})
80	78, 79	sseqtr4i 2145	. . . . . . 7 |- B (_ (A +o |^|S)
81	65, 80	jctir 300	. . . . . 6 |- (A (_ B -> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
82		eqss 2128	. . . . . 6 |- ((A +o |^|S) = B <-> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
83	81, 82	sylibr 207	. . . . 5 |- (A (_ B -> (A +o |^|S) = B)
84	83, 15	jctil 299	. . . 4 |- (A (_ B -> (|^|S e. On /\ (A +o |^|S) = B))
85		opreq2 4027	. . . . . 6 |- (x = |^|S -> (A +o x) = (A +o |^|S))
86	85	eqeq1d 1530	. . . . 5 |- (