Theorem prlem934 5119

Description: Lemma 9-3.4 of [Gleason] p. 122.

Assertion

Ref	Expression
prlem934	|- ((A e. P. /\ B e. Q.) -> E.x(x e. A /\ -. (x +Q B) e. A))

Distinct variable groups:   x,A   x,B

Proof of Theorem prlem934

Step	Hyp	Ref	Expression
1		prpssnq 5074	. . . . . . 7 |- (A e. P. -> A (. Q.)
2		dfpss3 2130	. . . . . . 7 |- (A (. Q. <-> (A (_ Q. /\ -. Q. (_ A))
3	1, 2	sylib 198	. . . . . 6 |- (A e. P. -> (A (_ Q. /\ -. Q. (_ A))
4	3	pm3.27d 325	. . . . 5 |- (A e. P. -> -. Q. (_ A)
5	4	adantl 388	. . . 4 |- ((B e. Q. /\ A e. P.) -> -. Q. (_ A)
6		df-nq 5018	. . . . . . . . . 10 |- Q. = ((N. X. N.)/. ~Q )
7		eleq1 1531	. . . . . . . . . . . 12 |- ([<.v, u>.] ~Q = y -> ([<.v, u>.] ~Q e. A <-> y e. A))
8	7	imbi2d 611	. . . . . . . . . . 11 |- ([<.v, u>.] ~Q = y -> ((A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> [<.v, u>.] ~Q e. A) <-> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> y e. A)))
9	8	imbi2d 611	. . . . . . . . . 10 |- ([<.v, u>.] ~Q = y -> ((A e. P. -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> [<.v, u>.] ~Q e. A)) <-> (A e. P. -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> y e. A))))
10		opreq2 3960	. . . . . . . . . . . . . . 15 |- ([<.z, w>.] ~Q = B -> (x +Q [<.z, w>.] ~Q ) = (x +Q B))
11	10	eleq1d 1537	. . . . . . . . . . . . . 14 |- ([<.z, w>.] ~Q = B -> ((x +Q [<.z, w>.] ~Q ) e. A <-> (x +Q B) e. A))
12	11	imbi2d 611	. . . . . . . . . . . . 13 |- ([<.z, w>.] ~Q = B -> ((x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) <-> (x e. A -> (x +Q B) e. A)))
13	12	albidv 1276	. . . . . . . . . . . 12 |- ([<.z, w>.] ~Q = B -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) <-> A.x(x e. A -> (x +Q B) e. A)))
14	13	imbi1d 612	. . . . . . . . . . 11 |- ([<.z, w>.] ~Q = B -> ((A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> y e. A) <-> (A.x(x e. A -> (x +Q B) e. A) -> y e. A)))
15	14	imbi2d 611	. . . . . . . . . 10 |- ([<.z, w>.] ~Q = B -> ((A e. P. -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> y e. A)) <-> (A e. P. -> (A.x(x e. A -> (x +Q B) e. A) -> y e. A))))
16		pm3.27 323	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. N. /\ w e. N.) -> w e. N.)
17	16, 16	jca 288	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. N. /\ w e. N.) -> (w e. N. /\ w e. N.))
18	17	anim1i 334	. . . . . . . . . . . . . . . . . . 19 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> ((w e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)))
19		an42 507	. . . . . . . . . . . . . . . . . . 19 |- (((w e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) <-> ((w e. N. /\ v e. N.) /\ (z e. N. /\ w e. N.)))
20	18, 19	sylib 198	. . . . . . . . . . . . . . . . . 18 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> ((w e. N. /\ v e. N.) /\ (z e. N. /\ w e. N.)))
21		mulclpi 5001	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. N. /\ v e. N.) -> (w .N v) e. N.)
22		enqex 5028	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~Q e. V
23		ecexg 4255	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ~Q e. V -> [<.z, w>.] ~Q e. V)
24	22, 23	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 |- [<.z, w>.] ~Q e. V
25	24	prlem934a 5117	. . . . . . . . . . . . . . . . . . . . . 22 |- ((w .N v) e. N. -> ((([<.z, w>.] ~Q e. Q. /\ A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A)) /\ y e. A) -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A))
26	25	exp4c 380	. . . . . . . . . . . . . . . . . . . . 21 |- ((w .N v) e. N. -> ([<.z, w>.] ~Q e. Q. -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y e. A -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A))))
27	22, 6	ecopqsi 4283	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. N. /\ w e. N.) -> [<.z, w>.] ~Q e. Q.)
28	26, 27	syl5 21	. . . . . . . . . . . . . . . . . . . 20 |- ((w .N v) e. N. -> ((z e. N. /\ w e. N.) -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y e. A -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A))))
29	21, 28	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((w e. N. /\ v e. N.) -> ((z e. N. /\ w e. N.) -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y e. A -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A))))
30	29	imp 350	. . . . . . . . . . . . . . . . . 18 |- (((w e. N. /\ v e. N.) /\ (z e. N. /\ w e. N.)) -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y e. A -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A)))
31	20, 30	syl 10	. . . . . . . . . . . . . . . . 17 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y e. A -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A)))
32	31	com23 32	. . . . . . . . . . . . . . . 16 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> (y e. A -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A)))
33	32	adantld 390	. . . . . . . . . . . . . . 15 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> ((A e. P. /\ y e. A) -> (A.x(x e. A -> (x +Q [<.z, w>.] ~Q ) e. A) -> (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A)))
34		prcdpq 5077	. . . . . . . . . . . . . . . . . . . . 21 |- ((A e. P. /\ (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) e. A) -> ([<.v, u>.] ~Q <Q (y +Q ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q )) -> [<.v, u>.] ~Q e. A))
35		oprex 3974	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) e. V
36		visset 1809	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- y e. V
37	35, 36	ltaddpq 5059	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) e. Q. /\ y e. Q.) -> ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) <Q (([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) +Q y))
38		1pi 4991	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 1o e. N.
39	22, 6	ecopqsi 4283	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((w .N v) e. N. /\ 1o e. N.) -> [<.(w .N v), 1o>.] ~Q e. Q.)
40	38, 39	mpan2 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w .N v) e. N. -> [<.(w .N v), 1o>.] ~Q e. Q.)
41	21, 40	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. N. /\ v e. N.) -> [<.(w .N v), 1o>.] ~Q e. Q.)
42	41, 27	anim12i 333	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((w e. N. /\ v e. N.) /\ (z e. N. /\ w e. N.)) -> ([<.(w .N v), 1o>.] ~Q e. Q. /\ [<.z, w>.] ~Q e. Q.))
43		mulclpq 5040	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (([<.(w .N v), 1o>.] ~Q e. Q. /\ [<.z, w>.] ~Q e. Q.) -> ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) e. Q.)
44	20, 42, 43	3syl 20	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) -> ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) e. Q.)
45	37, 44	sylan 448	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. N. /\ w e. N.)