Theorem oawordeulem 5236

Description: Lemma for oawordex 5239.

Hypotheses

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

Assertion

Ref	Expression
oawordeulem	|- (A C_ 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		opreq2 4890	. . . . . 6 |- (x = |^|S -> (A +o x) = (A +o |^|S))
2	1	eqeq1d 1892	. . . . 5 |- (x = |^|S -> ((A +o x) = B <-> (A +o |^|S) = B))
3	2	rcla4ev 2381	. . . 4 |- ((|^|S e. On /\ (A +o |^|S) = B) -> E.x e. On (A +o x) = B)
4		oawordeulem.3	. . . . . 6 |- S = {y e. On | B C_ (A +o y)}
5		ssrab2 2692	. . . . . 6 |- {y e. On | B C_ (A +o y)} C_ On
6	4, 5	eqsstri 2647	. . . . 5 |- S C_ On
7		opreq2 4890	. . . . . . . . 9 |- (y = B -> (A +o y) = (A +o B))
8	7	sseq2d 2645	. . . . . . . 8 |- (y = B -> (B C_ (A +o y) <-> B C_ (A +o B)))
9	8, 4	elrab2 2416	. . . . . . 7 |- (B e. S <-> (B e. On /\ B C_ (A +o B)))
10		oawordeulem.2	. . . . . . 7 |- B e. On
11		oawordeulem.1	. . . . . . . 8 |- A e. On
12		oaword2 5235	. . . . . . . 8 |- ((B e. On /\ A e. On) -> B C_ (A +o B))
13	10, 11, 12	mp2an 761	. . . . . . 7 |- B C_ (A +o B)
14	9, 10, 13	mpbir2an 800	. . . . . 6 |- B e. S
15		ne0i 2881	. . . . . 6 |- (B e. S -> S =/= (/))
16	14, 15	ax-mp 7	. . . . 5 |- S =/= (/)
17		oninton 3881	. . . . 5 |- ((S C_ On /\ S =/= (/)) -> |^|S e. On)
18	6, 16, 17	mp2an 761	. . . 4 |- |^|S e. On
19		onzsl 3928	. . . . . . . 8 |- (|^|S e. On <-> (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. _V /\ Lim |^|S)))
20	18, 19	mpbi 206	. . . . . . 7 |- (|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. _V /\ Lim |^|S))
21		opreq2 4890	. . . . . . . . . . 11 |- (|^|S = (/) -> (A +o |^|S) = (A +o (/)))
22		oa0 5200	. . . . . . . . . . . 12 |- (A e. On -> (A +o (/)) = A)
23	11, 22	ax-mp 7	. . . . . . . . . . 11 |- (A +o (/)) = A
24	21, 23	syl6eq 1944	. . . . . . . . . 10 |- (|^|S = (/) -> (A +o |^|S) = A)
25	24	sseq1d 2644	. . . . . . . . 9 |- (|^|S = (/) -> ((A +o |^|S) C_ B <-> A C_ B))
26	25	biimprd 171	. . . . . . . 8 |- (|^|S = (/) -> (A C_ B -> (A +o |^|S) C_ B))
27		opreq2 4890	. . . . . . . . . . . 12 |- (|^|S = suc z -> (A +o |^|S) = (A +o suc z))
28		oasuc 5208	. . . . . . . . . . . . 13 |- ((A e. On /\ z e. On) -> (A +o suc z) = suc (A +o z))
29	11, 28	mpan 759	. . . . . . . . . . . 12 |- (z e. On -> (A +o suc z) = suc (A +o z))
30	27, 29	sylan9eqr 1951	. . . . . . . . . . 11 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) = suc (A +o z))
31		visset 2295	. . . . . . . . . . . . . . 15 |- z e. _V
32	31	sucid 3744	. . . . . . . . . . . . . 14 |- z e. suc z
33		eleq2 1958	. . . . . . . . . . . . . 14 |- (|^|S = suc z -> (z e. |^|S <-> z e. suc z))
34	32, 33	mpbiri 211	. . . . . . . . . . . . 13 |- (|^|S = suc z -> z e. |^|S)
35	18	oneli 3777	. . . . . . . . . . . . . 14 |- (z e. |^|S -> z e. On)
36		opreq2 4890	. . . . . . . . . . . . . . . . . 18 |- (y = z -> (A +o y) = (A +o z))
37	36	sseq2d 2645	. . . . . . . . . . . . . . . . 17 |- (y = z -> (B C_ (A +o y) <-> B C_ (A +o z)))
38	37	onnminsb 3885	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z e. |^|{y e. On | B C_ (A +o y)} -> -. B C_ (A +o z)))
39	4	inteqi 3218	. . . . . . . . . . . . . . . . 17 |- |^|S = |^|{y e. On | B C_ (A +o y)}
40	39	eleq2i 1961	. . . . . . . . . . . . . . . 16 |- (z e. |^|S <-> z e. |^|{y e. On | B C_ (A +o y)})
41	38, 40	syl5ib 223	. . . . . . . . . . . . . . 15 |- (z e. On -> (z e. |^|S -> -. B C_ (A +o z)))
42		ontri1 3695	. . . . . . . . . . . . . . . . 17 |- ((B e. On /\ (A +o z) e. On) -> (B C_ (A +o z) <-> -. (A +o z) e. B))
43		oacl 5215	. . . . . . . . . . . . . . . . . 18 |- ((A e. On /\ z e. On) -> (A +o z) e. On)
44	11, 43	mpan 759	. . . . . . . . . . . . . . . . 17 |- (z e. On -> (A +o z) e. On)
45	42, 10, 44	sylancr 526	. . . . . . . . . . . . . . . 16 |- (z e. On -> (B C_ (A +o z) <-> -. (A +o z) e. B))
46	45	con2bid 585	. . . . . . . . . . . . . . 15 |- (z e. On -> ((A +o z) e. B <-> -. B C_ (A +o z)))
47	41, 46	sylibrd 221	. . . . . . . . . . . . . 14 |- (z e. On -> (z e. |^|S -> (A +o z) e. B))
48	35, 47	mpcom 60	. . . . . . . . . . . . 13 |- (z e. |^|S -> (A +o z) e. B)
49	10	onordi 3774	. . . . . . . . . . . . . 14 |- Ord B
50		ordsucss 3899	. . . . . . . . . . . . . 14 |- (Ord B -> ((A +o z) e. B -> suc (A +o z) C_ B))
51	49, 50	ax-mp 7	. . . . . . . . . . . . 13 |- ((A +o z) e. B -> suc (A +o z) C_ B)
52	34, 48, 51	3syl 24	. . . . . . . . . . . 12 |- (|^|S = suc z -> suc (A +o z) C_ B)
53	52	adantl 424	. . . . . . . . . . 11 |- ((z e. On /\ |^|S = suc z) -> suc (A +o z) C_ B)
54	30, 53	eqsstrd 2651	. . . . . . . . . 10 |- ((z e. On /\ |^|S = suc z) -> (A +o |^|S) C_ B)
55	54	r19.23aiva 2212	. . . . . . . . 9 |- (E.z e. On |^|S = suc z -> (A +o |^|S) C_ B)
56	55	a1d 15	. . . . . . . 8 |- (E.z e. On |^|S = suc z -> (A C_ B -> (A +o |^|S) C_ B))
57		iunss 3291	. . . . . . . . . . 11 |- (U_z e. |^|S(A +o z) C_ B <-> A.z e. |^|S(A +o z) C_ B)
58	10	onelssi 3778	. . . . . . . . . . . 12 |- ((A +o z) e. B -> (A +o z) C_ B)
59	48, 58	syl 12	. . . . . . . . . . 11 |- (z e. |^|S -> (A +o z) C_ B)
60	57, 59	mprgbir 2163	. . . . . . . . . 10 |- U_z e. |^|S(A +o z) C_ B
61		oalim 5212	. . . . . . . . . . . 12 |- ((A e. On /\ (|^|S e. _V /\ Lim |^|S)) -> (A +o |^|S) = U_z e. |^|S(A +o z))
62	11, 61	mpan 759	. . . . . . . . . . 11 |- ((|^|S e. _V /\ Lim |^|S) -> (A +o |^|S) = U_z e. |^|S(A +o z))
63	62	sseq1d 2644	. . . . . . . . . 10 |- ((|^|S e. _V /\ Lim |^|S) -> ((A +o |^|S) C_ B <-> U_z e. |^|S(A +o z) C_ B))
64	60, 63	mpbiri 211	. . . . . . . . 9 |- ((|^|S e. _V /\ Lim |^|S) -> (A +o |^|S) C_ B)
65	64	a1d 15	. . . . . . . 8 |- ((|^|S e. _V /\ Lim |^|S) -> (A C_ B -> (A +o |^|S) C_ B))
66	26, 56, 65	3jaoi 1160	. . . . . . 7 |- ((|^|S = (/) \/ E.z e. On |^|S = suc z \/ (|^|S e. _V /\ Lim |^|S)) -> (A C_ B -> (A +o |^|S) C_ B))
67	20, 66	ax-mp 7	. . . . . 6 |- (A C_ B -> (A +o |^|S) C_ B)
68	8	rcla4ev 2381	. . . . . . . . 9 |- ((B e. On /\ B C_ (A +o B)) -> E.y e. On B C_ (A +o y))
69	10, 13, 68	mp2an 761	. . . . . . . 8 |- E.y e. On B C_ (A +o y)
70		ax-17 1317	. . . . . . . . . 10 |- (z e. B -> A.y z e. B)
71		ax-17 1317	. . . . . . . . . . 11 |- (z e. A -> A.y z e. A)
72		ax-17 1317	. . . . . . . . . . 11 |- (z e. +o -> A.y z e. +o )
73		hbrab1 2257	. . . . . . . . . . . 12 |- (z e. {y e. On | B C_ (A +o y)} -> A.y z e. {y e. On | B C_ (A +o y)})
74	73	hbint 3225	. . . . . . . . . . 11 |- (z e. |^|{y e. On | B C_ (A +o y)} -> A.y z e. |^|{y e. On | B C_ (A +o y)})
75	71, 72, 74	hbopr 4904	. . . . . . . . . 10 |- (z e. (A +o |^|{y e. On | B C_ (A +o y)}) -> A.y z e. (A +o |^|{y e. On | B C_ (A +o y)}))
76	70, 75	hbss 2614	. . . . . . . . 9 |- (B C_ (A +o |^|{y e. On | B C_ (A +o y)}) -> A.y B C_ (A +o |^|{y e. On | B C_ (A +o y)}))
77		opreq2 4890	. . . . . . . . . 10 |- (y = |^|{y e. On | B C_ (A +o y)} -> (A +o y) = (A +o |^|{y e. On | B C_ (A +o y)}))
78	77	sseq2d 2645	. . . . . . . . 9 |- (y = |^|{y e. On | B C_ (A +o y)} -> (B C_ (A +o y) <-> B C_ (A +o |^|{y e. On | B C_ (A +o y)})))
79	76, 78	onminsb 3879	. . . . . . . 8 |- (E.y e. On B C_ (A +o y) -> B C_ (A +o |^|{y e. On | B C_ (A +o y)}))
80	69, 79	ax-mp 7	. . . . . . 7 |- B C_ (A +o |^|{y e. On | B C_ (A +o y)})
81	39	opreq2i 4893	. . . . . . 7 |- (A +o |^|S) = (A +o |^|{y e. On | B C_ (A +o y)})
82	80, 81	sseqtr4i 2650	. . . . . 6 |- B C_ (A +o |^|S)
83	67, 82	jctir 317	. . . . 5 |- (A C_ B -> ((A +o |^|S) C_ B /\ B C_ (A +o |^|S)))
84		eqss 2631	. . . . 5 |- ((A +o |^|S) = B <-> ((A +o |^|S) C_ B /\ B C_ (A +o |^|S)))
85	83, 84	sylibr 217	. . . 4 |- (A C_ B -> (A +o |^|S) = B)
86	3, 18, 85	sylancr 526	. . 3 |- (A C_ B -> E.x e. On (A +o x) = B)
87		oacan 5229	. . . . . 6 |- ((A e. On /\ x e. On /\ y e. On) -> ((A +o x) = (A +o y) <-> x = y))
88	11, 87	mp3an1 1178	. . . . 5 |- ((x e. On /\ y e. On) -> ((A +o x) = (A +o y) <-> x = y))
89		eqtr3 1907	. . . . 5 |- (((A +o x) = B /\ (A +o y) = B) -> (A +o x) = (A +o y))
90	88, 89	syl5bi 225	. . . 4 |- ((x e. On /\ y e. On) -> (((A +o x) = B /\ (A +o y) = B) -> x = y))
91	90	rgen2a 2160	. . 3 |- A.x e. On A.y e. On (((A +o x) = B /\ (A +o y) = B) -> x = y)
92	86, 91	jctir 317	. 2 |- (A C_ B -> (E.x e. On (A +o x) = B /\ A.x e. On A.y e. On (((A +o x) = B /\ (A +o y) = B) -> x = y)))
93		opreq2 4890	. . . 4 |- (x = y -> (A +o x) = (A +o y))
94	93	eqeq1d 1892	. . 3 |- (x = y -> ((A +o x) = B <-> (A +o y) = B))
95	94	reu4 2446	. 2 |- (E!x e. On (A +o x) = B <-> (E.x e. On (A +o x) = B /\ A.x e. On A.y e. On (((A +o x) = B /\ (A +o y) = B) -> x = y)))
96	92, 95	sylibr 217	1 |- (A C_ B -> E!x e. On (A +o x) = B)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  E!wreu 2107  {crab 2108  _Vcvv 2292   C_ wss 2593  (/)c0 2875  |^|cint 3214  U_ciun 3255  Ord word 3656  Oncon0 3657  Lim wlim 3658  suc csuc 3659  (class class class)co 4884   +o coa 5174

This theorem is referenced by:  oawordeu 5237

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-oprab 4887  df-rdg 5140  df-oadd 5179

Copyright terms: Public domain