Theorem reclem2pr 3951

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 group(s):   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 3950	. . . 4 |- (A e. P. -> (/) (. B)
3		prn0 3887	. . . . . . 7 |- (A e. P. -> -. A = (/))
4		elprpq 3889	. . . . . . . . . . . . . 14 |- ((A e. P. /\ z e. A) -> z e. Q.)
5		visset 1350	. . . . . . . . . . . . . . . . 17 |- z e. V
6	5	recrecpq 3867	. . . . . . . . . . . . . . . 16 |- (z e. Q. -> (*Q` (*Q` z)) = z)
7	6	eleq1d 1155	. . . . . . . . . . . . . . 15 |- (z e. Q. -> ((*Q` (*Q` z)) e. A <-> z e. A))
8	7	anbi2d 468	. . . . . . . . . . . . . 14 |- (z e. Q. -> ((A e. P. /\ (*Q` (*Q` z)) e. A) <-> (A e. P. /\ z e. A)))
9	4, 8	syl 12	. . . . . . . . . . . . 13 |- ((A e. P. /\ z e. A) -> ((A e. P. /\ (*Q` (*Q` z)) e. A) <-> (A e. P. /\ z e. A)))
10		fvex 2838	. . . . . . . . . . . . . 14 |- (*Q` z) e. V
11		fveq2 2832	. . . . . . . . . . . . . . . 16 |- (x = (*Q` z) -> (*Q` x) = (*Q` (*Q` z)))
12	11	eleq1d 1155	. . . . . . . . . . . . . . 15 |- (x = (*Q` z) -> ((*Q` x) e. A <-> (*Q` (*Q` z)) e. A))
13	12	anbi2d 468	. . . . . . . . . . . . . 14 |- (x = (*Q` z) -> ((A e. P. /\ (*Q` x) e. A) <-> (A e. P. /\ (*Q` (*Q` z)) e. A)))
14	10, 13	cla4ev 1401	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` (*Q` z)) e. A) -> E.x(A e. P. /\ (*Q` x) e. A))
15	9, 14	syl6bir 188	. . . . . . . . . . . 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 58	. . . . . . . . . . 11 |- ((A e. P. /\ z e. A) -> E.x(A e. P. /\ (*Q` x) e. A))
17		elprpq 3889	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> (*Q` x) e. Q.)
18		dmrecpq 3868	. . . . . . . . . . . . . . 15 |- dom *Q = Q.
19		0npq 3844	. . . . . . . . . . . . . . 15 |- -. (/) e. Q.
20	18, 19	ndmfvrcl 2849	. . . . . . . . . . . . . 14 |- ((*Q` x) e. Q. -> x e. Q.)
21	17, 20	syl 12	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` x) e. A) -> x e. Q.)
22		prcdpq 3891	. . . . . . . . . . . . . . . 16 |- ((A e. P. /\ (*Q` x) e. A) -> ((*Q` y) <Q (*Q` x) -> (*Q` y) e. A))
23		visset 1350	. . . . . . . . . . . . . . . . 17 |- x e. V
24		visset 1350	. . . . . . . . . . . . . . . . 17 |- y e. V
25	23, 24	ltrpq 3879	. . . . . . . . . . . . . . . 16 |- (x <Q y -> (*Q` y) <Q (*Q` x))
26	22, 25	syl5 22	. . . . . . . . . . . . . . 15 |- ((A e. P. /\ (*Q` x) e. A) -> (x <Q y -> (*Q` y) e. A))
27	26	19.21aiv 943	. . . . . . . . . . . . . 14 |- ((A e. P. /\ (*Q` x) e. A) -> A.y(x <Q y -> (*Q` y) e. A))
28	1	cleqabi 1176	. . . . . . . . . . . . . . . 16 |- (x e. B <-> E.y(x <Q y /\ -. (*Q` y) e. A))
29		exanali 725	. . . . . . . . . . . . . . . 16 |- (E.y(x <Q y /\ -. (*Q` y) e. A) <-> -. A.y(x <Q y -> (*Q` y) e. A))
30	28, 29	bitr 151	. . . . . . . . . . . . . . 15 |- (x e. B <-> -. A.y(x <Q y -> (*Q` y) e. A))
31	30	bicon2i 194	. . . . . . . . . . . . . 14 |- (A.y(x <Q y -> (*Q` y) e. A) <-> -. x e. B)
32	27, 31	sylib 173	. . . . . . . . . . . . 13 |- ((A e. P. /\ (*Q` x) e. A) -> -. x e. B)
33	21, 32	jca 236	. . . . . . . . . . . 12 |- ((A e. P. /\ (*Q` x) e. A) -> (x e. Q. /\ -. x e. B))
34	33	19.22i 723	. . . . . . . . . . 11 |- (E.x(A e. P. /\ (*Q` x) e. A) -> E.x(x e. Q. /\ -. x e. B))
35	16, 34	syl 12	. . . . . . . . . 10 |- ((A e. P. /\ z e. A) -> E.x(x e. Q. /\ -. x e. B))
36	35	exp 291	. . . . . . . . 9 |- (A e. P. -> (z e. A -> E.x(x e. Q. /\ -. x e. B)))
37	36	19.23adv 954	. . . . . . . 8 |- (A e. P. -> (E.z z e. A -> E.x(x e. Q. /\ -. x e. B)))
38		n0 1714	. . . . . . . 8 |- (-. A = (/) <-> E.z z e. A)
39		nss 1550	. . . . . . . 8 |- (-. Q. (_ B <-> E.x(x e. Q. /\ -. x e. B))
40	37, 38, 39	3imtr4g 426	. . . . . . 7 |- (A e. P. -> (-. A = (/) -> -. Q. (_ B))
41	3, 40	mpd 46	. . . . . 6 |- (A e. P. -> -. Q. (_ B)
42		ltrelpq 3845	. . . . . . . . . . . 12 |- <Q (_ (Q. X. Q.)
43	24, 42	brel 2459	. . . . . . . . . . 11 |- (x <Q y -> (x e. Q. /\ y e. Q.))
44	43	pm3.26d 258	. . . . . . . . . 10 |- (x <Q y -> x e. Q.)
45	44	adantr 306	. . . . . . . . 9 |- ((x <Q y /\ -. (*Q` y) e. A) -> x e. Q.)
46	45	19.23aiv 952	. . . . . . . 8 |- (E.y(x <Q y /\ -. (*Q` y) e. A) -> x e. Q.)
47	28, 46	sylbi 174	. . . . . . 7 |- (x e. B -> x e. Q.)
48	47	ssriv 1508	. . . . . 6 |- B (_ Q.
49	41, 48	jctil 240	. . . . 5 |- (A e. P. -> (B (_ Q. /\ -. Q. (_ B))
50		dfpss3 1558	. . . . 5 |- (B (. Q. <-> (B (_ Q. /\ -. Q. (_ B))
51	49, 50	sylibr 175	. . . 4 |- (A e. P. -> B (. Q.)
52	2, 51	jca 236	. . 3 |- (A e. P. -> ((/) (. B /\ B (. Q.))
53		ltsopq 3869	. . . . . . . . . . . 12 |- <Q Or Q.
54	5, 53, 42, 23, 24	sotri 2630	. . . . . . . . . . 11 |- ((z <Q x /\ x <Q y) -> z <Q y)
55	54	exp 291	. . . . . . . . . 10 |- (z <Q x -> (x <Q y -> z <Q y))
56	55	anim1d 432	. . . . . . . . 9 |- (z <Q x -> ((x <Q y /\ -. (*Q` y) e. A) -> (z <Q y /\ -. (*Q` y) e. A)))
57	56	19.22dv 947	. . . . . . . 8 |- (z <Q x -> (E.y(x <Q y /\ -. (*Q` y) e. A) -> E.y(z <Q y /\ -. (*Q` y) e. A)))
58		breq1 2065	. . . . . . . . . . 11 |- (x = z -> (x <Q y <-> z <Q y))
59	58	anbi1d 469	. . . . . . . . . 10 |- (x = z -> ((x <Q y /\ -. (*Q` y) e. A) <-> (z <Q y /\ -. (*Q` y) e. A)))
60	59	biexdv 936	. . . . . . . . 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 1419	. . . . . . . 8 |- (z e. B <-> E.y(z <Q y /\ -. (*Q` y) e. A))
62	57, 28, 61	3imtr4g 426	. . . . . . 7 |- (z <Q x -> (x e. B -> z e. B))
63	62	com12 13	. . . . . 6 |- (x e. B -> (z <Q x -> z e. B))
64	63	19.21aiv 943	. . . . 5 |- (x e. B -> A.z(z <Q x -> z e. B))
65	23, 24	ltbtwnpq 3878	. . . . . . . . . 10 |- (x <Q y -> E.z(x <Q z /\ z <Q y))
66	65	anim1i 269	. . . . . . . . 9 |- ((x <Q y /\ -. (*Q` y) e. A) -> (E.z(x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
67		19.41v 963	. . . . . . . . 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 175	. . . . . . . 8 |- ((x <Q y /\ -. (*Q` y) e. A) -> E.z((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
69	68	19.22i 723	. . . . . . 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 963	. . . . . . . . . 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 336	. . . . . . . . . . . 12 |- (((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> (x <Q z /\ (z <Q y /\ -. (*Q` y) e. A)))
72		ancom 333	. . . . . . . . . . . 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 151	. . . . . . . . . . 11 |- (((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> ((z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
74	73	biex 733	. . . . . . . . . 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 368	. . . . . . . . . 10 |- ((z e. B /\ x <Q z) <-> (E.y(z <Q y /\ -. (*Q` y) e. A) /\ x <Q z))
76	70, 74, 75	3bitr4 158	. . . . . . . . 9 |- (E.y((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> (z e. B /\ x <Q z))
77	76	biex 733	. . . . . . . 8 |- (E.zE.y((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> E.z(z e. B /\ x <Q z))
78		excom 728	. . . . . . . 8 |- (E.zE.y((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A) <-> E.yE.z((x <Q z /\ z <Q y) /\ -. (*Q` y) e. A))
79	77, 78	bitr3 153	. . . . . . 7 |- (E.z(z e. B /\ x <Q z)