Theorem oawordeulem 4188

Description: Lemma for oawordex 4191.

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 2131	. . . . . . . . . . 11 |- {y e. On | B (_ (A +o y)} (_ On
3	1, 2	eqsstr 2091	. . . . . . . . . 10 |- S (_ On
4		opreq2 3969	. . . . . . . . . . . . . 14 |- (y = B -> (A +o y) = (A +o B))
5	4	sseq2d 2089	. . . . . . . . . . . . 13 |- (y = B -> (B (_ (A +o y) <-> B (_ (A +o B)))
6	5, 1	elrab2 1907	. . . . . . . . . . . 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 4187	. . . . . . . . . . . . 13 |- ((B e. On /\ A e. On) -> B (_ (A +o B))
10	7, 8, 9	mp2an 697	. . . . . . . . . . . 12 |- B (_ (A +o B)
11	6, 7, 10	mpbir2an 730	. . . . . . . . . . 11 |- B e. S
12		ne0i 2286	. . . . . . . . . . 11 |- (B e. S -> S =/= (/))
13	11, 12	ax-mp 7	. . . . . . . . . 10 |- S =/= (/)
14		oninton 3012	. . . . . . . . . 10 |- ((S (_ On /\ S =/= (/)) -> |^|S e. On)
15	3, 13, 14	mp2an 697	. . . . . . . . 9 |- |^|S e. On
16		onzsl 3117	. . . . . . . . 9 |- (|^|S e. On <-> (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S)))
17	15, 16	mpbi 189	. . . . . . . 8 |- (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. V /\ Lim |^|S))
18		opreq2 3969	. . . . . . . . . . . 12 |- (|^|S = (/) -> (A +o |^|S) = (A +o (/)))
19		oa0 4155	. . . . . . . . . . . . 13 |- (A e. On -> (A +o (/)) = A)
20	8, 19	ax-mp 7	. . . . . . . . . . . 12 |- (A +o (/)) = A
21	18, 20	syl6eq 1523	. . . . . . . . . . 11 |- (|^|S = (/) -> (A +o |^|S) = A)
22	21	sseq1d 2088	. . . . . . . . . 10 |- (|^|S = (/) -> ((A +o |^|S) (_ B <-> A (_ B))
23	22	biimprd 154	. . . . . . . . 9 |- (|^|S = (/) -> (A (_ B -> (A +o |^|S) (_ B))
24		opreq2 3969	. . . . . . . . . . . . 13 |- (|^|S = suc z -> (A +o |^|S) = (A +o suc z))
25		oasuc 4163	. . . . . . . . . . . . . 14 |- ((A e. On /\ z e. On) -> (A +o suc z) = suc (A +o z))
26	8, 25	mpan 695	. . . . . . . . . . . . 13 |- (z e. On -> (A +o suc z) = suc (A +o z))
27	24, 26	sylan9eqr 1529	. . . . . . . . . . . 12 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) = suc (A +o z))
28		visset 1813	. . . . . . . . . . . . . . . 16 |- z e. V
29	28	sucid 3051	. . . . . . . . . . . . . . 15 |- z e. suc z
30		eleq2 1535	. . . . . . . . . . . . . . 15 |- (|^|S = suc z -> (z e. |^|S <-> z e. suc z))
31	29, 30	mpbiri 194	. . . . . . . . . . . . . 14 |- (|^|S = suc z -> z e. |^|S)
32	15	onel 3098	. . . . . . . . . . . . . . 15 |- (z e. |^|S -> z e. On)
33		opreq2 3969	. . . . . . . . . . . . . . . . . . 19 |- (y = z -> (A +o y) = (A +o z))
34	33	sseq2d 2089	. . . . . . . . . . . . . . . . . 18 |- (y = z -> (B (_ (A +o y) <-> B (_ (A +o z)))
35	34	onnminsb 3016	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (z e. |^|{y e. On | B (_ (A +o y)} -> -. B (_ (A +o z)))
36	1	inteqi 2537	. . . . . . . . . . . . . . . . . 18 |- |^|S = |^|{y e. On | B (_ (A +o y)}
37	36	eleq2i 1538	. . . . . . . . . . . . . . . . 17 |- (z e. |^|S <-> z e. |^|{y e. On | B (_ (A +o y)})
38	35, 37	syl5ib 206	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z e. |^|S -> -. B (_ (A +o z)))
39		oacl 4170	. . . . . . . . . . . . . . . . . . 19 |- ((A e. On /\ z e. On) -> (A +o z) e. On)
40	8, 39	mpan 695	. . . . . . . . . . . . . . . . . 18 |- (z e. On -> (A +o z) e. On)
41		ontri1 2981	. . . . . . . . . . . . . . . . . . 19 |- ((B e. On /\ (A +o z) e. On) -> (B (_ (A +o z) <-> -. (A +o z) e. B))
42	7, 41	mpan 695	. . . . . . . . . . . . . . . . . 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 526	. . . . . . . . . . . . . . . 16 |- (z e. On -> ((A +o z) e. B <-> -. B (_ (A +o z)))
45	38, 44	sylibrd 204	. . . . . . . . . . . . . . 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	onord 3095	. . . . . . . . . . . . . . 15 |- Ord B
48		ordsucss 3069	. . . . . . . . . . . . . . 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 388	. . . . . . . . . . . 12 |- ((z e. On /\ |^|S = suc z) -> suc (A +o z) (_ B)
52	27, 51	eqsstrd 2095	. . . . . . . . . . 11 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) (_ B)
53	52	r19.23aiva 1744	. . . . . . . . . 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 2591	. . . . . . . . . . . 12 |- (U_z e. |^|S(A +o z) (_ B <-> A.z e. |^|S(A +o z) (_ B)
56	7	onelss 3100	. . . . . . . . . . . . 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 1701	. . . . . . . . . . 11 |- U_z e. |^|S(A +o z) (_ B
59		oalim 4167	. . . . . . . . . . . . 13 |- ((A e. On /\ (|^|S e. V /\ Lim |^|S)) -> (A +o |^|S) = U_z e. |^|S(A +o z))
60	8, 59	mpan 695	. . . . . . . . . . . 12 |- ((|^|S e. V /\ Lim |^|S) -> (A +o |^|S) = U_z e. |^|S(A +o z))
61	60	sseq1d 2088	. . . . . . . . . . 11 |- ((|^|S e. V /\ Lim |^|S) -> ((A +o |^|S) (_ B <-> U_z e. |^|S(A +o z) (_ B))
62	58, 61	mpbiri 194	. . . . . . . . . 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 887	. . . . . . . 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 1877	. . . . . . . . . 10 |- ((B e. On /\ B (_ (A +o B)) -> E.y e. On B (_ (A +o y))
67	7, 10, 66	mp2an 697	. . . . . . . . 9 |- E.y e. On B (_ (A +o y)
68		ax-17 971	. . . . . . . . . . 11 |- (z e. B -> A.y z e. B)
69		ax-17 971	. . . . . . . . . . . 12 |- (z e. A -> A.y z e. A)
70		ax-17 971	. . . . . . . . . . . 12 |- (z e. +o -> A.y z e. +o )
71		hbrab1 1772	. . . . . . . . . . . . 13 |- (z e. {y e. On | B (_ (A +o y)} -> A.y z e. {y e. On | B (_ (A +o y)})
72	71	hbint 2543	. . . . . . . . . . . 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 3981	. . . . . . . . . . 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 2062	. . . . . . . . . 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 3969	. . . . . . . . . . 11 |- (y = |^|{y e. On | B (_ (A +o y)} -> (A +o y) = (A +o |^|{y e. On | B (_ (A +o y)}))
76	75	sseq2d 2089	. . . . . . . . . 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 3009	. . . . . . . . 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 3972	. . . . . . . 8 |- (A +o |^|S) = (A +o |^|{y e. On | B (_ (A +o y)})
80	78, 79	sseqtr4 2094	. . . . . . 7 |- B (_ (A +o |^|S)
81	65, 80	jctir 293	. . . . . 6 |- (A (_ B -> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
82		eqss 2077	. . . . . 6 |- ((A +o |^|S) = B <-> ((A +o |^|S) (_ B /\ B (_ (A +o |^|S)))
83	81, 82	sylibr 200	. . . . 5 |- (A (_ B -> (A +o |^|S) = B)
84	83, 15	jctil 292	. . . 4 |- (A (_ B -> (|^|S e. On /\ (A +o |^|S) = B))
85		opreq2 3969	. . . . . 6 |- (x = |^|S -> (A +o x) = (A +o |^|S))
86	85	eqeq1d 1483	. . . . 5 |- (