Theorem prlem934 3933

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 group(s):   x,A   x,B

Proof of Theorem prlem934

Step	Hyp	Ref	Expression
1		prpssnq 3888	. . . . . . 7 |- (A e. P. -> A (. Q.)
2		dfpss3 1558	. . . . . . 7 |- (A (. Q. <-> (A (_ Q. /\ -. Q. (_ A))
3	1, 2	sylib 173	. . . . . 6 |- (A e. P. -> (A (_ Q. /\ -. Q. (_ A))
4	3	pm3.27d 262	. . . . 5 |- (A e. P. -> -. Q. (_ A)
5	4	adantl 305	. . . 4 |- ((B e. Q. /\ A e. P.) -> -. Q. (_ A)
6		df-nq 3832	. . . . . . . . . 10 |- Q. = ((N. X. N.)/. ~Q )
7		eleq1 1149	. . . . . . . . . . . 12 |- ([<.v, u>.] ~Q = y -> ([<.v, u>.] ~Q e. A <-> y e. A))
8	7	imbi2d 464	. . . . . . . . . . 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 464	. . . . . . . . . 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 3007	. . . . . . . . . . . . . . 15 |- ([<.z, w>.] ~Q = B -> (x +Q [<.z, w>.] ~Q ) = (x +Q B))
11	10	eleq1d 1155	. . . . . . . . . . . . . 14 |- ([<.z, w>.] ~Q = B -> ((x +Q [<.z, w>.] ~Q ) e. A <-> (x +Q B) e. A))
12	11	imbi2d 464	. . . . . . . . . . . . 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	bialdv 935	. . . . . . . . . . . 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 465	. . . . . . . . . . 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 464	. . . . . . . . . 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 260	. . . . . . . . . . . . . . . . . . . . 21 |- ((u e. N. /\ w e. N.) -> w e. N.)
17	16, 16	jca 236	. . . . . . . . . . . . . . . . . . . 20 |- ((u e. N. /\ w e. N.) -> (w e. N. /\ w e. N.))
18	17	anim1i 269	. . . . . . . . . . . . . . . . . . 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 389	. . . . . . . . . . . . . . . . . . 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 173	. . . . . . . . . . . . . . . . . 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 3815	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. N. /\ v e. N.) -> (w .N v) e. N.)
22		enqex 3842	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ~Q e. V
23		ecexg 3204	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ~Q e. V -> [<.z, w>.] ~Q e. V)
24	22, 23	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . 23 |- [<.z, w>.] ~Q e. V
25	24	prlem934a 3931	. . . . . . . . . . . . . . . . . . . . . 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 297	. . . . . . . . . . . . . . . . . . . . 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 3230	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. N. /\ w e. N.) -> [<.z, w>.] ~Q e. Q.)
28	26, 27	syl5 22	. . . . . . . . . . . . . . . . . . . 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 12	. . . . . . . . . . . . . . . . . . 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 277	. . . . . . . . . . . . . . . . . 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 12	. . . . . . . . . . . . . . . . 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 307	. . . . . . . . . . . . . . 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 3891	. . . . . . . . . . . . . . . . . . . . 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 3018	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) e. V
36		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- y e. V
37	35, 36	ltaddpq 3873	. . . . . . . . . . . . . . . . . . . . . . . 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 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- 1o e. N.
39	22, 6	ecopqsi 3230	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((w .N v) e. N. /\ 1o e. N.) -> [<.(w .N v), 1o>.] ~Q e. Q.)
40	38, 39	mpan2 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((w .N v) e. N. -> [<.(w .N v), 1o>.] ~Q e. Q.)
41	21, 40	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w e. N. /\ v e. N.) -> [<.(w .N v), 1o>.] ~Q e. Q.)
42	41, 27	anim12i 268	. . . . . . . . . . . . . . . . . . . . . . . . 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 3854	. . . . . . . . . . . . . . . . . . . . . . . . 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 21	. . . . . . . . . . . . . . . . . . . . . . . 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 343	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((u e. N. /\ w e. N.) /\ (v e. N. /\ z e. N.)) /\ y e. Q.) -> ([<.(w .N v), 1o>.] ~Q .Q [<.z, w>.] ~Q ) <Q (([<.(w .N v), 1o