Theorem reclem3pr 3952

Description: Lemma for Proposition 9-3.7(v) of [Gleason] p. 124.

Hypothesis

Ref	Expression
reclempr.1	|- B = {x | E.y(x <Q y /\ -. (*Q` y) e. A)}

Assertion

Ref	Expression
reclem3pr	|- (A e. P. -> 1P (_ (A .P B))

Distinct variable group(s):   x,y,A   x,B

Proof of Theorem reclem3pr

Step	Hyp	Ref	Expression
1		fvex 2838	. . . . . . . . . 10 |- (*Q` w) e. V
2	1	prlem936 3949	. . . . . . . . 9 |- ((A e. P. /\ 1Q <Q (*Q` w)) -> E.v(v e. A /\ -. (v .Q (*Q` w)) e. A))
3		oprex 3018	. . . . . . . . . . . . . . . . . . 19 |- ((*Q` z) .Q w) e. V
4	3	isseti 1352	. . . . . . . . . . . . . . . . . 18 |- E.x x = ((*Q` z) .Q w)
5		fvex 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (*Q` z) e. V
6		fvex 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (*Q` v) e. V
7		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- x e. V
8		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- y e. V
9	7, 8	ltmpq 3871	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u e. Q. -> (x <Q y <-> (u .Q x) <Q (u .Q y)))
10		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- w e. V
11	7, 8	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (x .Q y) = (y .Q x)
12	5, 6, 9, 10, 11	caoprord2 3071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (w e. Q. -> ((*Q` z) <Q (*Q` v) <-> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
13		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- v e. V
14		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- z e. V
15	13, 14	ltrpq 3879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v <Q z -> (*Q` z) <Q (*Q` v))
16	12, 15	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w e. Q. -> (v <Q z -> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
17	16	adantl 305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. Q. /\ w e. Q.) -> (v <Q z -> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
18		recidpq 3865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (v e. Q. -> (v .Q (*Q` v)) = 1Q)
19	13, 6	mulcompq 3858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (v .Q (*Q` v)) = ((*Q` v) .Q v)
20	18, 19	syl5eqr 1138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v e. Q. -> ((*Q` v) .Q v) = 1Q)
21		recidpq 3865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (w e. Q. -> (w .Q (*Q` w)) = 1Q)
22	20, 21	opreqan12d 3015	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((v e. Q. /\ w e. Q.) -> (((*Q` v) .Q v) .Q (w .Q (*Q` w))) = (1Q .Q 1Q))
23		visset 1350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- u e. V
24	8, 23	mulasspq 3859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((x .Q y) .Q u) = (x .Q (y .Q u))
25	6, 13, 10, 11, 24, 1	caopr4 3078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((*Q` v) .Q v) .Q (w .Q (*Q` w))) = (((*Q` v) .Q w) .Q (v .Q (*Q` w)))
26		1q 3851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- 1Q e. Q.
27		mulidpq 3863	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (1Q e. Q. -> (1Q .Q 1Q) = 1Q)
28	26, 27	ax-mp 6	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (1Q .Q 1Q) = 1Q
29	22, 25, 28	3eqtr3g 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((v e. Q. /\ w e. Q.) -> (((*Q` v) .Q w) .Q (v .Q (*Q` w))) = 1Q)
30		mulclpq 3854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (((*Q` v) e. Q. /\ w e. Q.) -> ((*Q` v) .Q w) e. Q.)
31		recclpq 3866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v e. Q. -> (*Q` v) e. Q.)
32	30, 31	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((v e. Q. /\ w e. Q.) -> ((*Q` v) .Q w) e. Q.)
33		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v .Q (*Q` w)) e. V
34	33	recmulpq 3864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((*Q` v) .Q w) e. Q. -> ((*Q` ((*Q` v) .Q w)) = (v .Q (*Q` w)) <-> (((*Q` v) .Q w) .Q (v .Q (*Q` w))) = 1Q))
35	32, 34	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((v e. Q. /\ w e. Q.) -> ((*Q` ((*Q` v) .Q w)) = (v .Q (*Q` w)) <-> (((*Q` v) .Q w) .Q (v .Q (*Q` w))) = 1Q))
36	29, 35	mpbird 171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((v e. Q. /\ w e. Q.) -> (*Q` ((*Q` v) .Q w)) = (v .Q (*Q` w)))
37	36	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((v e. Q. /\ w e. Q.) -> ((*Q` ((*Q` v) .Q w)) e. A <-> (v .Q (*Q` w)) e. A))
38	37	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((v e. Q. /\ w e. Q.) -> (-. (*Q` ((*Q` v) .Q w)) e. A <-> -. (v .Q (*Q` w)) e. A))
39	38	biimprd 136	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. Q. /\ w e. Q.) -> (-. (v .Q (*Q` w)) e. A -> -. (*Q` ((*Q` v) .Q w)) e. A))
40	17, 39	anim12d 431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((v e. Q. /\ w e. Q.) -> ((v <Q z /\ -. (v .Q (*Q` w)) e. A) -> (((*Q` z) .Q w) <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A)))
41		breq1 2065	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = ((*Q` z) .Q w) -> (x <Q ((*Q` v) .Q w) <-> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
42	41	anbi1d 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = ((*Q` z) .Q w) -> ((x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A) <-> (((*Q` z) .Q w) <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A)))
43	42	biimprcd 138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((((*Q` z) .Q w) <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A) -> (x = ((*Q` z) .Q w) -> (x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A)))
44	40, 43	syl6 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((v e. Q. /\ w e. Q.) -> ((v <Q z /\ -. (v .Q (*Q` w)) e. A) -> (x = ((*Q` z) .Q w) -> (x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A))))
45		oprex 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((*Q` v) .Q w) e. V
46		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = ((*Q` v) .Q w) -> (x <Q y <-> x <Q ((*Q` v) .Q w)))
47		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y = ((*Q` v) .Q w) -> (*Q` y) = (*Q` ((*Q` v) .Q w)))
48	47	eleq1d 1155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = ((*Q` v) .Q w) -> ((*Q` y) e. A <-> (*Q` ((*Q` v) .Q w)) e. A))
49	48	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = ((*Q` v) .Q w) -> (-. (*Q` y) e. A <-> -. (*Q` ((*Q` v) .Q w)) e. A))
50	46, 49	anbi12d 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = ((*Q` v) .Q w) -> ((x <Q y /\ -. (*Q` y) e. A) <-> (x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A)))
51	45, 50	cla4ev 1401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A) -> E.y(x <Q y /\ -. (*Q` y) e. A))
52		reclempr.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- B = {x | E.y(x <Q y /\ -. (*Q` y) e. A)}
53	52	cleqabi 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. B <-> E.y(x <Q y /\ -. (*Q` y) e. A))
54	51, 53	sylibr 175	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A) -> x e. B)
55	44, 54	syl8 25	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((v e. Q. /\ w e. Q.) -> ((v <Q z /\ -. (v .Q (*Q` w)) e. A) -> (x = ((*Q` z) .Q w) -> x e. B)))
56		ltrelpq 3845	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <Q (_ (Q. X. Q.)
57	14, 56	brel 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (v <Q z -> (v e. Q. /\ z e. Q.))
58	57	pm3.26d 258	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v <Q z -> v e. Q.)
59	55, 58	sylan 343	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((v <Q z /\ w e. Q.) -> ((v <Q z /\ -. (v .Q (*Q` w)) e. A) -> (x = ((*Q` z) .Q w) -> x e. B)))
60	59	exp4b 296	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v <Q z -> (w e. Q. -> (v <Q z -> (-. (v .Q (*Q` w)) e. A -> (x = ((*Q` z) .Q w) -> x e. B)))))
61	60	pm2.43a 60	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (v <Q z -> (w e. Q. -> (-. (v .Q (*Q` w)) e. A -> (x = ((*Q` z) .Q w) -> x e. B))))
62	61	imp42 287	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((v <Q z /\ (w e. Q. /\ -. (v .Q (*Q` w)) e. A)) /\ x = ((*Q` z) .Q w)) -> x e. B)
63	62	anim2i 270	. . . . . . . . . . . . . . . . . . . . . 22 |- ((z e. A /\ ((v <Q z /\ (w e. Q. /\ -. (v .Q (*Q` w)) e. A)) /\ x = ((*Q` z) .Q w))) -> (z e. A /\ x e. B))
64		opreq2 3007	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = ((*Q` z) .Q w) -> (z