Theorem reclem2pr 5129

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 5128	. . . 4 |- (A e. P. -> (/) (. B)
3		prn0 5065	. . . . . . 7 |- (A e. P. -> A =/= (/))
4		elprpq 5067	. . . . . . . . . . . . . 14 |- ((A e. P. /\ z e. A) -> z e. Q.)
5		visset 1804	. . . . . . . . . . . . . . . . 17 |- z e. V
6	5	recrecpq 5045	. . . . . . . . . . . . . . . 16 |- (z e. Q. -> (*Q` (*Q` z)) = z)
7	6	eleq1d 1532	. . . . . . . . . . . . . . 15 |- (z e. Q. -> ((*Q` (*Q` z)) e. A <-> z e. A))
8	7	anbi2d 614	. . . . . . . . . . . . . 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 3717	. . . . . . . . . . . . . 14 |- (*Q` z) e. V
11		fveq2 3709	. . . . . . . . . . . . . . . 16 |- (x = (*Q` z) -> (*Q` x) = (*Q` (*Q` z)))
12	11	eleq1d 1532	. . . . . . . . . . . . . . 15 |- (x = (*Q` z) -> ((*Q` x) e. A <-> (*Q` (*Q` z)) e. A))
13	12	anbi2d 614	. . . . . . . . . . . . . 14 |- (x = (*Q` z) -> ((A e. P. /\ (*Q` x) e. A) <-> (A e. P. /\ (*Q` (*Q` z)) e. A)))
14	10, 13	cla4ev 1860	. . . . . . . . . . . . 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 5067	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> (*Q` x) e. Q.)
18		dmrecpq 5046	. . . . . . . . . . . . . . 15 |- dom *Q = Q.
19		0npq 5022	. . . . . . . . . . . . . . 15 |- -. (/) e. Q.
20	18, 19	ndmfvrcl 3731	. . . . . . . . . . . . . 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 5069	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ (*Q` x) e. A) -> ((*Q` y) <Q (*Q` x) -> (*Q` y) e. A))
23		visset 1804	. . . . . . . . . . . . . . . . 17 |- x e. V
24		visset 1804	. . . . . . . . . . . . . . . . 17 |- y e. V
25	23, 24	ltrpq 5057	. . . . . . . . . . . . . . . 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 1281	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> A.y(x <Q y -> (*Q` y) e. A))
28	1	abeq2i 1562	. . . . . . . . . . . . . . . 16 |- (x e. B <-> E.y(x <Q y /\ -. (*Q` y) e. A))
29		exanali 1039	. . . . . . . . . . . . . . . 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 1036	. . . . . . . . . . 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 1209	. . . . . . . 8 |- (A e. P. -> (E.z z e. A -> E.x(x e. Q. /\ -. x e. B)))
38		ne0 2278	. . . . . . . 8 |- (A =/= (/) <-> E.z z e. A)
39		nss 2103	. . . . . . . 8 |- (-. Q. (_ B <-> E.x(x e. Q. /\ -. x e. B))
40	37, 38, 39	3imtr4g 551	. . . . . . 7 |- (A e. P. -> (A =/= (/) -> -. Q. (_ B))
41	3, 40	mpd 26	. . . . . 6 |- (A e. P. -> -. Q. (_ B)
42		ltrelpq 5023	. . . . . . . . . . . 12 |- <Q (_ (Q. X. Q.)
43	24, 42	brel 3213	. . . . . . . . . . 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 1290	. . . . . . . 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 2059	. . . . . 6 |- B (_ Q.
49	41, 48	jctil 292	. . . . 5 |- (A e. P. -> (B (_ Q. /\ -. Q. (_ B))
50		dfpss3 2124	. . . . 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 5047	. . . . . . . . . . . 12 |- <Q Or Q.
54	5, 53, 42, 23, 24	sotri 3429	. . . . . . . . . . 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 558	. . . . . . . . 9 |- (z <Q x -> ((x <Q y /\ -. (*Q` y) e. A) -> (z <Q y /\ -. (*Q` y) e. A)))
57	56	19.22dv 1285	. . . . . . . 8 |- (z <Q x -> (E.y(x <Q y /\ -. (*Q` y) e. A) -> E.y(z <Q y /\ -. (*Q` y) e. A)))
58		breq1 2612	. . . . . . . . . . 11 |- (x = z -> (x <Q y <-> z <Q y))
59	58	anbi1d 615	. . . . . . . . . 10 |- (x = z -> ((x <Q y /\ -. (*Q` y) e. A) <-> (z <Q y /\ -. (*Q` y) e. A)))
60	59	exbidv 1274	. . . . . . . . 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 1892	. . . . . . . 8 |- (z e. B <-> E.y(z <Q y /\ -. (*Q` y) e. A))
62	57, 28, 61	3imtr4g 551	. . . . . . 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 1281	. . . . 5 |- (x e. B -> A.z(z <Q x -> z e. B))
65	23, 24	ltbtwnpq 5056	. . . . . . . . . 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 1300	. . . . . . . . 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 1036	. . . . . . 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 1300	. . . . . . . . . 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 1047	. . . . . . . . . 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 480	. . . . . . . . . 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 1047	. . . . . . . 8 |- (E.zE.y((x <Q z /\ z <Q y) /\ -.