Theorem reclem3pr 5130

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 groups:   x,y,A   x,B

Proof of Theorem reclem3pr

Step	Hyp	Ref	Expression
1		fvex 3717	. . . . . . . . . 10 |- (*Q` w) e. V
2	1	prlem936 5127	. . . . . . . . 9 |- ((A e. P. /\ 1Q <Q (*Q` w)) -> E.v(v e. A /\ -. (v .Q (*Q` w)) e. A))
3		oprex 3968	. . . . . . . . . . . . . . . . . 18 |- ((*Q` z) .Q w) e. V
4	3	isseti 1806	. . . . . . . . . . . . . . . . 17 |- E.x x = ((*Q` z) .Q w)
5		fvex 3717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (*Q` z) e. V
6		fvex 3717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (*Q` v) e. V
7		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- x e. V
8		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- y e. V
9	7, 8	ltmpq 5049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u e. Q. -> (x <Q y <-> (u .Q x) <Q (u .Q y)))
10		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- w e. V
11	7, 8	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x .Q y) = (y .Q x)
12	5, 6, 9, 10, 11	caoprord2 4043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (w e. Q. -> ((*Q` z) <Q (*Q` v) <-> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
13		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- v e. V
14		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- z e. V
15	13, 14	ltrpq 5057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v <Q z -> (*Q` z) <Q (*Q` v))
16	12, 15	syl5bi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (w e. Q. -> (v <Q z -> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
17	16	adantl 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((v e. Q. /\ w e. Q.) -> (v <Q z -> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
18		recidpq 5043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v e. Q. -> (v .Q (*Q` v)) = 1Q)
19	13, 6	mulcompq 5036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (v .Q (*Q` v)) = ((*Q` v) .Q v)
20	18, 19	syl5eqr 1513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v e. Q. -> ((*Q` v) .Q v) = 1Q)
21		recidpq 5043	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (w e. Q. -> (w .Q (*Q` w)) = 1Q)
22	20, 21	opreqan12d 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((v e. Q. /\ w e. Q.) -> (((*Q` v) .Q v) .Q (w .Q (*Q` w))) = (1Q .Q 1Q))
23		visset 1804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- u e. V
24	8, 23	mulasspq 5037	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((x .Q y) .Q u) = (x .Q (y .Q u))
25	6, 13, 10, 11, 24, 1	caopr4 4050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((*Q` v) .Q v) .Q (w .Q (*Q` w))) = (((*Q` v) .Q w) .Q (v .Q (*Q` w)))
26		1q 5029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- 1Q e. Q.
27		mulidpq 5041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (1Q e. Q. -> (1Q .Q 1Q) = 1Q)
28	26, 27	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (1Q .Q 1Q) = 1Q
29	22, 25, 28	3eqtr3g 1522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((v e. Q. /\ w e. Q.) -> (((*Q` v) .Q w) .Q (v .Q (*Q` w))) = 1Q)
30		mulclpq 5032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((*Q` v) e. Q. /\ w e. Q.) -> ((*Q` v) .Q w) e. Q.)
31		recclpq 5044	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v e. Q. -> (*Q` v) e. Q.)
32	30, 31	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((v e. Q. /\ w e. Q.) -> ((*Q` v) .Q w) e. Q.)
33		oprex 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v .Q (*Q` w)) e. V
34	33	recmulpq 5042	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((*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 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((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 196	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((v e. Q. /\ w e. Q.) -> (*Q` ((*Q` v) .Q w)) = (v .Q (*Q` w)))
37	36	eleq1d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((v e. Q. /\ w e. Q.) -> ((*Q` ((*Q` v) .Q w)) e. A <-> (v .Q (*Q` w)) e. A))
38	37	negbid 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((v e. Q. /\ w e. Q.) -> (-. (*Q` ((*Q` v) .Q w)) e. A <-> -. (v .Q (*Q` w)) e. A))
39	38	biimprd 154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((v e. Q. /\ w e. Q.) -> (-. (v .Q (*Q` w)) e. A -> -. (*Q` ((*Q` v) .Q w)) e. A))
40	17, 39	anim12d 556	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((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 2612	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = ((*Q` z) .Q w) -> (x <Q ((*Q` v) .Q w) <-> ((*Q` z) .Q w) <Q ((*Q` v) .Q w)))
42	41	anbi1d 615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (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 156	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((((*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 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((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 3968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((*Q` v) .Q w) e. V
46		breq2 2613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = ((*Q` v) .Q w) -> (x <Q y <-> x <Q ((*Q` v) .Q w)))
47		fveq2 3709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = ((*Q` v) .Q w) -> (*Q` y) = (*Q` ((*Q` v) .Q w)))
48	47	eleq1d 1532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = ((*Q` v) .Q w) -> ((*Q` y) e. A <-> (*Q` ((*Q` v) .Q w)) e. A))
49	48	negbid 609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = ((*Q` v) .Q w) -> (-. (*Q` y) e. A <-> -. (*Q` ((*Q` v) .Q w)) e. A))
50	46, 49	anbi12d 626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (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 1860	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((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	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- B = {x | E.y(x <Q y /\ -. (*Q` y) e. A)}
53	52	abeq2i 1562	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. B <-> E.y(x <Q y /\ -. (*Q` y) e. A))
54	51, 53	sylibr 200	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((x <Q ((*Q` v) .Q w) /\ -. (*Q` ((*Q` v) .Q w)) e. A) -> x e. B)
55	44, 54	syl8 24	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((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 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- <Q (_ (Q. X. Q.)
57	14, 56	brel 3213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v <Q z -> (v e. Q. /\ z e. Q.))
58	57	pm3.26d 321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v <Q z -> v e. Q.)
59	55, 58	sylan 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((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 379	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (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 66	. . . . . . . . . . . . . . . . . . . . . . 23 |- (v <Q z -> (w e. Q. -> (-. (v .Q (*Q` w)) e. A -> (x = ((*Q` z) .Q w) -> x e. B))))
62	61	imp42 369	. . . . . . . . . . . . . . . . . . . . . 22 |- (((v <Q z /\ (w e. Q. /\ -. (v .Q (*Q` w)) e. A)) /\ x = ((*Q` z) .Q w)) -> x e. B)
63	62	anim2i 335	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. A /\ (