Theorem reclem2pr 5157

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

Hypothesis

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

Assertion

Ref	Expression
reclem2pr	|- (A e. P. -> B e. P.)

Distinct variable groups:   x,y,A   x,B

Proof of Theorem reclem2pr

Step	Hyp	Ref	Expression
1		reclempr.1	. . . . 5 |- B = {x | E.y(x <Q y /\ -. (*Q` y) e. A)}
2	1	reclem1pr 5156	. . . 4 |- (A e. P. -> (/) (. B)
3		prn0 5093	. . . . . . 7 |- (A e. P. -> A =/= (/))
4		elprpq 5095	. . . . . . . . . . . . . 14 |- ((A e. P. /\ z e. A) -> z e. Q.)
5		visset 1813	. . . . . . . . . . . . . . . . 17 |- z e. V
6	5	recrecpq 5073	. . . . . . . . . . . . . . . 16 |- (z e. Q. -> (*Q` (*Q` z)) = z)
7	6	eleq1d 1540	. . . . . . . . . . . . . . 15 |- (z e. Q. -> ((*Q` (*Q` z)) e. A <-> z e. A))
8	7	anbi2d 616	. . . . . . . . . . . . . 14 |- (z e. Q. -> ((A e. P. /\ (*Q` (*Q` z)) e. A) <-> (A e. P. /\ z e. A)))
9	4, 8	syl 10	. . . . . . . . . . . . 13 |- ((A e. P. /\ z e. A) -> ((A e. P. /\ (*Q` (*Q` z)) e. A) <-> (A e. P. /\ z e. A)))
10		fvex 3732	. . . . . . . . . . . . . 14 |- (*Q` z) e. V
11		fveq2 3724	. . . . . . . . . . . . . . . 16 |- (x = (*Q` z) -> (*Q` x) = (*Q` (*Q` z)))
12	11	eleq1d 1540	. . . . . . . . . . . . . . 15 |- (x = (*Q` z) -> ((*Q` x) e. A <-> (*Q` (*Q` z)) e. A))
13	12	anbi2d 616	. . . . . . . . . . . . . 14 |- (x = (*Q` z) -> ((A e. P. /\ (*Q` x) e. A) <-> (A e. P. /\ (*Q` (*Q` z)) e. A)))
14	10, 13	cla4ev 1869	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` (*Q` z)) e. A) -> E.x(A e. P. /\ (*Q` x) e. A))
15	9, 14	syl6bir 215	. . . . . . . . . . . 12 |- ((A e. P. /\ z e. A) -> ((A e. P. /\ z e. A) -> E.x(A e. P. /\ (*Q` x) e. A)))
16	15	pm2.43i 64	. . . . . . . . . . 11 |- ((A e. P. /\ z e. A) -> E.x(A e. P. /\ (*Q` x) e. A))
17		elprpq 5095	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> (*Q` x) e. Q.)
18		dmrecpq 5074	. . . . . . . . . . . . . . 15 |- dom *Q = Q.
19		0npq 5050	. . . . . . . . . . . . . . 15 |- -. (/) e. Q.
20	18, 19	ndmfvrcl 3746	. . . . . . . . . . . . . 14 |- ((*Q` x) e. Q. -> x e. Q.)
21	17, 20	syl 10	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` x) e. A) -> x e. Q.)
22		prcdpq 5097	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ (*Q` x) e. A) -> ((*Q` y) <Q (*Q` x) -> (*Q` y) e. A))
23		visset 1813	. . . . . . . . . . . . . . . . 17 |- x e. V
24		visset 1813	. . . . . . . . . . . . . . . . 17 |- y e. V
25	23, 24	ltrpq 5085	. . . . . . . . . . . . . . . 16 |- (x <Q y -> (*Q` y) <Q (*Q` x))
26	22, 25	syl5 21	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ (*Q` x) e. A) -> (x <Q y -> (*Q` y) e. A))
27	26	19.21aiv 1286	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> A.y(x <Q y -> (*Q` y) e. A))
28	1	abeq2i 1570	. . . . . . . . . . . . . . . 16 |- (x e. B <-> E.y(x <Q y /\ -. (*Q` y) e. A))
29		exanali 1043	. . . . . . . . . . . . . . . 16 |- (E.y(x <Q y /\ -. (*Q` y) e. A) <-> -. A.y(x <Q y -> (*Q` y) e. A))
30	28, 29	bitr 173	. . . . . . . . . . . . . . 15 |- (x e. B <-> -. A.y(x <Q y -> (*Q` y) e. A))
31	30	con2bii 221	. . . . . . . . . . . . . 14 |- (A.y(x <Q y -> (*Q` y) e. A) <-> -. x e. B)
32	27, 31	sylib 198	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` x) e. A) -> -. x e. B)
33	21, 32	jca 288	. . . . . . . . . . . 12 |- ((A e. P. /\ (*Q` x) e. A) -> (x e. Q. /\ -. x e. B))
34	33	19.22i 1040	. . . . . . . . . . 11 |- (E.x(A e. P. /\ (*Q` x) e. A) -> E.x(x e. Q. /\ -. x e. B))
35	16, 34	syl 10	. . . . . . . . . 10 |- ((A e. P. /\ z e. A) -> E.x(x e. Q. /\ -. x e. B))
36	35	ex 373	. . . . . . . . 9 |- (A e. P. -> (z e. A -> E.x(x e. Q. /\ -. x e. B)))
37	36	19.23adv 1214	. . . . . . . 8 |- (A e. P. -> (E.z z e. A -> E.x(x e. Q. /\ -. x e. B)))
38		ne0 2288	. . . . . . . 8 |- (A =/= (/) <-> E.z z e. A)
39		nss 2113	. . . . . . . 8 |- (-. Q. (_ B <-> E.x(x e. Q. /\ -. x e. B))
40	37, 38, 39	3imtr4g 553	. . . . . . 7 |- (A e. P. -> (A =/= (/) -> -. Q. (_ B))
41	3, 40	mpd 26	. . . . . 6 |- (A e. P. -> -. Q. (_ B)
42		ltrelpq 5051	. . . . . . . . . . . 12 |- <Q (_ (Q. X. Q.)
43	24, 42	brel 3223	. . . . . . . . . . 11 |- (x <Q y -> (x e. Q. /\ y e. Q.))
44	43	pm3.26d 321	. . . . . . . . . 10 |- (x <Q y -> x e. Q.)
45	44	adantr 389	. . . . . . . . 9 |- ((x <Q y /\ -. (*Q` y) e. A) -> x e. Q.)
46	45	19.23aiv 1295	. . . . . . . 8 |- (E.y(x <Q y /\ -. (*Q` y) e. A) -> x e. Q.)
47	28, 46	sylbi 199	. . . . . . 7 |- (x e. B -> x e. Q.)
48	47	ssriv 2069	. . . . . 6 |- B (_ Q.
49	41, 48	jctil 292	. . . . 5 |- (A e. P. -> (B (_ Q. /\ -. Q. (_ B))
50		dfpss3 2134	. . . . 5 |- (B (. Q. <-> (B (_ Q. /\ -. Q. (_ B))
51	49, 50	sylibr 200	. . . 4 |- (A e. P. -> B (. Q.)
52	2, 51	jca 288	. . 3 |- (A e. P. -> ((/) (. B /\ B (. Q.))
53		ltsopq 5075	. . . . . . . . . . . 12 |- <Q Or Q.
54	5, 53, 42, 23, 24	sotri 3443	. . . . . . . . . . 11 |- ((z <Q x /\ x <Q y) -> z <Q y)
55	54	ex 373	. . . . . . . . . 10 |- (z <Q x -> (x <Q y -> z <Q y))
56	55	anim1d 560	. . . . . . . . 9 |- (z <Q x -> ((x <Q y /\ -. (*Q` y) e. A) -> (z <Q y /\ -. (*Q` y) e. A)))
57	56	19.22dv 1290	. . . . . . . 8 |- (z <Q x -> (E.y(x <Q y /\ -. (*Q` y) e. A) -> E.y(z <Q y /\ -. (*Q` y) e. A)))
58		breq1 2622	. . . . . . . . . . 11 |- (x = z -> (x <Q y <-> z <Q y))
59	58	anbi1d 617	. . . . . . . . . 10 |- (x = z -> ((x <Q y /\ -. (*Q` y) e. A) <-> (z <Q y /\ -. (*Q` y) e. A)))
60	59	exbidv 1279	. . . . . . . . 9 |- (x = z -> (E.y(x <Q y /\ -. (*Q` y) e. A) <-> E.y(z <Q y /\ -. (*Q` y) e. A)))
61	5, 60, 1	elab2 1901	. . . . . . . 8 |- (z e. B <-> E.y(z <Q y /\ -. (*Q` y) e. A))
62	57, 28, 61	3imtr4g 553	. . . . . . 7 |- (z <Q x -> (x e. B -> z e. B))
63	62	com12 11	. . . . . 6 |- (x e. B -> (z <Q x -> z e. B))
64	63	19.21aiv 1286	. . . . 5 |- (x e. B -> A.z(z <Q x -> z e. B))
65	23, 24	ltbtwnpq 5084	. . . . . . . . . 10 |- (x <Q y -> E.z(x <Q z /\ z <Q y))
66	65	anim1i 334	. . . . . . . . 9 |- ((x <Q y /\ -. (*Q` y) e. A) -> (E.z(x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
67		19.41v 1305	. . . . . . . . 9 |- (E.z((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> (E.z(x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
68	66, 67	sylibr 200	. . . . . . . 8 |- ((x <Q y /\ -. (*Q` y) e. A) -> E.z((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
69	68	19.22i 1040	. . . . . . 7 |- (E.y(x <Q y /\ -. (*Q` y) e. A) -> E.yE.z((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
70		19.41v 1305	. . . . . . . . . 10 |- (E.y((z <Q y /\ -. (*Q` y) e. A) /\ x <Q z) <-> (E.y(z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
71		anass 439	. . . . . . . . . . . 12 |- (((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> (x <Q z /\ (z <Q y /\ -. (*Q` y) e. A)))
72		ancom 435	. . . . . . . . . . . 12 |- ((x <Q z /\ (z <Q y /\ -. (*Q` y) e. A)) <-> ((z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
73	71, 72	bitr 173	. . . . . . . . . . 11 |- (((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> ((z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
74	73	exbii 1051	. . . . . . . . . 10 |- (E.y((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> E.y((z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
75	61	anbi1i 481	. . . . . . . . . 10 |- ((z e. B /\ x <Q z) <-> (E.y(z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
76	70, 74, 75	3bitr4 183	. . . . . . . . 9 |- (E.y((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> (z e. B /\ x <Q z))
77	76	exbii 1051	. . . . . . . 8 |- (E.zE.y((x <Q z /\ z <Q y) /\