Theorem oawordeulem 3156

Description: Lemma for oawordex 3159.

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 group(s):   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		ssrab 1556	. . . . . . . . . . 11 |- {y e. On | B (_ (A +o y)} (_ On
3	1, 2	eqsstr 1530	. . . . . . . . . 10 |- S (_ On
4		oawordeulem.2	. . . . . . . . . . . . 13 |- B e. On
5		oawordeulem.1	. . . . . . . . . . . . 13 |- A e. On
6		oaword2 3155	. . . . . . . . . . . . 13 |- ((B e. On /\ A e. On) -> B (_ (A +o B))
7	4, 5, 6	mp2an 520	. . . . . . . . . . . 12 |- B (_ (A +o B)
8	1	eleq2i 1153	. . . . . . . . . . . . . 14 |- (B e. S <-> B e. {y e. On | B (_ (A +o y)})
9		opreq2 3007	. . . . . . . . . . . . . . . 16 |- (y = B -> (A +o y) = (A +o B))
10	9	sseq2d 1528	. . . . . . . . . . . . . . 15 |- (y = B -> (B (_ (A +o y) <-> B (_ (A +o B)))
11	10	elrab 1422	. . . . . . . . . . . . . 14 |- (B e. {y e. On | B (_ (A +o y)} <-> (B e. On /\ B (_ (A +o B)))
12	8, 11	bitr 151	. . . . . . . . . . . . 13 |- (B e. S <-> (B e. On /\ B (_ (A +o B)))
13	12, 4	mpbiran 547	. . . . . . . . . . . 12 |- (B e. S <-> B (_ (A +o B))
14	7, 13	mpbir 165	. . . . . . . . . . 11 |- B e. S
15		n0i 1712	. . . . . . . . . . 11 |- (B e. S -> -. S = (/))
16	14, 15	ax-mp 6	. . . . . . . . . 10 |- -. S = (/)
17		oninton 2267	. . . . . . . . . 10 |- ((S (_ On /\ -. S = (/)) -> |^|S e. On)
18	3, 16, 17	mp2an 520	. . . . . . . . 9 |- |^|S e. On
19		onzsl 2367	. . . . . . . . 9 |- (|^|S e. On <-> (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S)))
20	18, 19	mpbi 164	. . . . . . . 8 |- (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S))
21		opreq2 3007	. . . . . . . . . . . 12 |- (|^|S = (/) -> (A +o |^|S) = (A +o (/)))
22		oa0 3124	. . . . . . . . . . . . 13 |- (A e. On -> (A +o (/)) = A)
23	5, 22	ax-mp 6	. . . . . . . . . . . 12 |- (A +o (/)) = A
24	21, 23	syl6eq 1140	. . . . . . . . . . 11 |- (|^|S = (/) -> (A +o |^|S) = A)
25	24	sseq1d 1527	. . . . . . . . . 10 |- (|^|S = (/) -> ((A +o |^|S) (_ B <-> A (_ B))
26	25	biimprd 136	. . . . . . . . 9 |- (|^|S = (/) -> (A (_ B -> (A +o |^|S) (_ B))
27		opreq2 3007	. . . . . . . . . . . . . 14 |- (|^|S = suc z -> (A +o |^|S) = (A +o suc z))
28		oasuc 3131	. . . . . . . . . . . . . . 15 |- ((A e. On /\ z e. On) -> (A +o suc z) = suc (A +o z))
29	5, 28	mpan 518	. . . . . . . . . . . . . 14 |- (z e. On -> (A +o suc z) = suc (A +o z))
30	27, 29	sylan9eqr 1145	. . . . . . . . . . . . 13 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) = suc (A +o z))
31		visset 1350	. . . . . . . . . . . . . . . . 17 |- z e. V
32	31	sucid 2304	. . . . . . . . . . . . . . . 16 |- z e. suc z
33		eleq2 1150	. . . . . . . . . . . . . . . 16 |- (|^|S = suc z -> (z e. |^|S <-> z e. suc z))
34	32, 33	mpbiri 169	. . . . . . . . . . . . . . 15 |- (|^|S = suc z -> z e. |^|S)
35	18	onel 2346	. . . . . . . . . . . . . . . 16 |- (z e. |^|S -> z e. On)
36		opreq2 3007	. . . . . . . . . . . . . . . . . . . 20 |- (y = z -> (A +o y) = (A +o z))
37	36	sseq2d 1528	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (B (_ (A +o y) <-> B (_ (A +o z)))
38	37	onnminsb 2271	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> (z e. |^|{y e. On | B (_ (A +o y)} -> -. B (_ (A +o z)))
39	1	inteqi 1969	. . . . . . . . . . . . . . . . . . 19 |- |^|S = |^|{y e. On | B (_ (A +o y)}
40	39	eleq2i 1153	. . . . . . . . . . . . . . . . . 18 |- (z e. |^|S <-> z e. |^|{y e. On | B (_ (A +o y)})
41	38, 40	syl5ib 181	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (z e. |^|S -> -. B (_ (A +o z)))
42		oacl 3138	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. On /\ z e. On) -> (A +o z) e. On)
43	5, 42	mpan 518	. . . . . . . . . . . . . . . . . . 19 |- (z e. On -> (A +o z) e. On)
44		ontri1 2232	. . . . . . . . . . . . . . . . . . . 20 |- ((B e. On /\ (A +o z) e. On) -> (B (_ (A +o z) <-> -. (A +o z) e. B))
45	4, 44	mpan 518	. . . . . . . . . . . . . . . . . . 19 |- ((A +o z) e. On -> (B (_ (A +o z) <-> -. (A +o z) e. B))
46	43, 45	syl 12	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> (B (_ (A +o z) <-> -. (A +o z) e. B))
47	46	bicon2d 404	. . . . . . . . . . . . . . . . 17 |- (z e. On -> ((A +o z) e. B <-> -. B (_ (A +o z)))
48	41, 47	sylibrd 179	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z e. |^|S -> (A +o z) e. B))
49	35, 48	mpcom 49	. . . . . . . . . . . . . . 15 |- (z e. |^|S -> (A +o z) e. B)
50	4	onord 2343	. . . . . . . . . . . . . . . 16 |- Ord B
51		ordsucss 2320	. . . . . . . . . . . . . . . 16 |- (Ord B -> ((A +o z) e. B -> suc (A +o z) (_ B))
52	50, 51	ax-mp 6	. . . . . . . . . . . . . . 15 |- ((A +o z) e. B -> suc (A +o z) (_ B)
53	34, 49, 52	3syl 21	. . . . . . . . . . . . . 14 |- (|^|S = suc z -> suc (A +o z) (_ B)
54	53	adantl 305	. . . . . . . . . . . . 13 |- ((z e. On /\ |^|S = suc z) -> suc (A +o z) (_ B)
55	30, 54	eqsstrd 1534	. . . . . . . . . . . 12 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) (_ B)
56	55	exp 291	. . . . . . . . . . 11 |- (z e. On -> (|^|S = suc z -> (A +o |^|S) (_ B))
57	56	r19.23aiv 1284	. . . . . . . . . 10 |- (E.z e. On |^|S = suc z -> (A +o |^|S) (_ B)
58	57	a1d 14	. . . . . . . . 9 |- (E.z e. On |^|S = suc z -> (A (_ B -> (A +o |^|S) (_ B))
59		iunss 2017	. . . . . . . . . . . 12 |- (U.z e. |^| S(A +o z) (_ B <-> A.z e. |^| S(A +o z) (_ B)
60	4	onelss 2348	. . . . . . . . . . . . 13 |- ((A +o z) e. B -> (A +o z) (_ B)
61	49, 60	syl 12	. . . . . . . . . . . 12 |- (z e. |^|S -> (A +o z) (_ B)
62	59, 61	mprgbir 1250	. . . . . . . . . . 11 |- U.z e. |^| S(A +o z) (_ B
63		oalim 3135	. . . . . . . . . . . . 13 |- ((A e. On /\ (|^|S e. V /\ Lim |^|S)) -> (A +o |^|S) = U.z e. |^| S(A +o z))
64	5, 63	mpan 518	. . . . . . . . . . . 12 |- ((|^|S e. V /\ Lim |^|S) -> (A +o |^|S) = U.z e. |^| S(A +o z))
65	64	sseq1d 1527	. . . . . . . . . . 11 |- ((|^|S e. V /\ Lim |^|S) -> ((A +o |^|S) (_ B <-> U.z e. |^| S(A +o z) (_ B))
66	62, 65	mpbiri 169	. . . . . . . . . 10 |- ((|^|S e. V /\ Lim |^|S) -> (A +o |^|S) (_ B)
67	66	a1d 14	. . . . . . . . 9 |- ((|^|S e. V /\ Lim |^|S) -> (A (_ B -> (A +o |^|S) (_ B))
68	26, 58, 67	3jaoi 633	. . . . . . . 8 |- ((|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S)) -> (A (_ B -> (A +o |^|S) (_ B))
69	20, 68	ax-mp 6	. . . . . . 7 |- (A (_ B -> (A +o |^|S) (_ B)
70	10	rcla4ev 1403	. . . . . . . . . 10 |- ((B e. On /\ B (_ (A +o B)) -> E.y e. On B (_ (A +o y))
71	4, 7, 70	mp2an 520	. . . . . . . . 9 |- E.y e. On B (_ (A +o y)
72		ax-17 925	. . . . . . . . . . 11 |- (z e. B -> A.y z e. B)
73		ax-17 925	. . . . . . . . . . . 12 |- (z e. A -> A.y z e. A)
74		ax-17 925	. . . . . . . . . . . 12 |- (z e. +o -> A.y z e. +o )
75		hbrab1 1310	. . . . . . . . . . . . 13 |- (z e. {y e. On | B (_ (A +o y)} -> A.y z e. {y e. On | B (_ (A +o y)})
76	75	hbint 1975	. . . . . . . . . . . 12 |- (z e. |^|{y e. On | B (_ (A +o y)} -> A.y z e. |^|{y e. On | B (_ (A +o y)})
77	73, 74, 76	hbopr 3017	. . . . . . . . . . 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)}))
78	72, 77	hbss 1501	. . . . . . . . . 10 |- (B (_ (A +o |^|{y e. On | B (_ (A +o y)}) -> A.y B (_ (A +o |^|{y e. On | B (_ (A +o y)}))
79		opreq2 3007	. . . . . . . . . . 11 |- (y = |^|{y e. On | B (_ (A +o y)} -> (A +o y) = (A +o |^|{y e. On | B (_ (A +o y)}))
80	79	sseq2d 1528	. . . . . . . . . 10 |- (y = |^|{y e. On | B (_ (A +o y)} -> (B (_ (A +o y) <-> B (_ (A +o |^|{y e. On | B (_ (A +o y)})))
81	78, 80	onminsb 2264	. . . . . . . . 9 |- (E.y e. On B (_ (A +o y) -> B (_ (A +o |^|{y e. On | B (_ (A +o y)}))
82	71, 81	ax-mp 6	. . . . . . . 8 |- B (_ (A +o |^|{y e. On | B (_ (A +o y)})
83	39	opreq2i 3010	. . . . . . . 8 |- (A +o |^|S) = (A +o |^|{y e. On | B (_ (A +o y)})
84	82, 83	sseqtr4 1533	. . . . . . 7 |- B (_ (A +o |^|S)
85	69, 84	jctir 241	. . . . . 6 |- (A (_ B -> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
86		eqss 1516	. . . . . 6 |- ((A +o |^|S) = B <-> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
87	85, 86	sylibr 175	. . . . 5 |- (A (_ B -> (A +o |^|S) = B)
88	87, 18	jctil 240	. . . 4 |- (A (_ B -> (|^|S e. On /\ (A +o |^|S) = B))
89		opreq2 3007	. . . . . 6 |- (x = |^|S -> (A +o x) = (A