Metamath Proof Explorer

Theorem reclem2pr

Description: Lemma for Proposition 9-3.7 of Gleason p. 124. (Contributed by NM, 30-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypothesis reclempr.1 
|- B = { x | E. y ( x
Assertion reclem2pr 
|- ( A e. P. -> B e. P. )

Proof

Step Hyp Ref Expression
1 reclempr.1 
 |-  B = { x | E. y ( x
2 prpssnq 
 |-  ( A e. P. -> A C. Q. )
3 pssnel 
 |-  ( A C. Q. -> E. x ( x e. Q. /\ -. x e. A ) )
4 recclnq 
 |-  ( x e. Q. -> ( *Q ` x ) e. Q. )
5 nsmallnq 
 |-  ( ( *Q ` x ) e. Q. -> E. z z
6 4 5 syl 
 |-  ( x e. Q. -> E. z z
7 6 adantr 
 |-  ( ( x e. Q. /\ -. x e. A ) -> E. z z
8 recrecnq 
 |-  ( x e. Q. -> ( *Q ` ( *Q ` x ) ) = x )
9 8 eleq1d 
 |-  ( x e. Q. -> ( ( *Q ` ( *Q ` x ) ) e. A <-> x e. A ) )
10 9 notbid 
 |-  ( x e. Q. -> ( -. ( *Q ` ( *Q ` x ) ) e. A <-> -. x e. A ) )
11 10 anbi2d 
 |-  ( x e. Q. -> ( ( z  ( z
12 fvex 
 |-  ( *Q ` x ) e. _V
13 breq2 
 |-  ( y = ( *Q ` x ) -> ( z  z
14 fveq2 
 |-  ( y = ( *Q ` x ) -> ( *Q ` y ) = ( *Q ` ( *Q ` x ) ) )
15 14 eleq1d 
 |-  ( y = ( *Q ` x ) -> ( ( *Q ` y ) e. A <-> ( *Q ` ( *Q ` x ) ) e. A ) )
16 15 notbid 
 |-  ( y = ( *Q ` x ) -> ( -. ( *Q ` y ) e. A <-> -. ( *Q ` ( *Q ` x ) ) e. A ) )
17 13 16 anbi12d 
 |-  ( y = ( *Q ` x ) -> ( ( z  ( z
18 12 17 spcev 
 |-  ( ( z  E. y ( z
19 11 18 syl6bir 
 |-  ( x e. Q. -> ( ( z  E. y ( z
20 vex 
 |-  z e. _V
21 breq1 
 |-  ( x = z -> ( x  z
22 21 anbi1d 
 |-  ( x = z -> ( ( x  ( z
23 22 exbidv 
 |-  ( x = z -> ( E. y ( x  E. y ( z
24 20 23 1 elab2 
 |-  ( z e. B <-> E. y ( z
25 19 24 syl6ibr 
 |-  ( x e. Q. -> ( ( z  z e. B ) )
26 25 expcomd 
 |-  ( x e. Q. -> ( -. x e. A -> ( z  z e. B ) ) )
27 26 imp 
 |-  ( ( x e. Q. /\ -. x e. A ) -> ( z  z e. B ) )
28 27 eximdv 
 |-  ( ( x e. Q. /\ -. x e. A ) -> ( E. z z  E. z z e. B ) )
29 7 28 mpd 
 |-  ( ( x e. Q. /\ -. x e. A ) -> E. z z e. B )
30 n0 
 |-  ( B =/= (/) <-> E. z z e. B )
31 29 30 sylibr 
 |-  ( ( x e. Q. /\ -. x e. A ) -> B =/= (/) )
32 31 exlimiv 
 |-  ( E. x ( x e. Q. /\ -. x e. A ) -> B =/= (/) )
33 2 3 32 3syl 
 |-  ( A e. P. -> B =/= (/) )
34 0pss 
 |-  ( (/) C. B <-> B =/= (/) )
35 33 34 sylibr 
 |-  ( A e. P. -> (/) C. B )
36 prn0 
 |-  ( A e. P. -> A =/= (/) )
37 elprnq 
 |-  ( ( A e. P. /\ z e. A ) -> z e. Q. )
38 recrecnq 
 |-  ( z e. Q. -> ( *Q ` ( *Q ` z ) ) = z )
39 38 eleq1d 
 |-  ( z e. Q. -> ( ( *Q ` ( *Q ` z ) ) e. A <-> z e. A ) )
40 39 anbi2d 
 |-  ( z e. Q. -> ( ( A e. P. /\ ( *Q ` ( *Q ` z ) ) e. A ) <-> ( A e. P. /\ z e. A ) ) )
41 37 40 syl 
 |-  ( ( A e. P. /\ z e. A ) -> ( ( A e. P. /\ ( *Q ` ( *Q ` z ) ) e. A ) <-> ( A e. P. /\ z e. A ) ) )
42 fvex 
 |-  ( *Q ` z ) e. _V
43 fveq2 
 |-  ( x = ( *Q ` z ) -> ( *Q ` x ) = ( *Q ` ( *Q ` z ) ) )
44 43 eleq1d 
 |-  ( x = ( *Q ` z ) -> ( ( *Q ` x ) e. A <-> ( *Q ` ( *Q ` z ) ) e. A ) )
45 44 anbi2d 
 |-  ( x = ( *Q ` z ) -> ( ( A e. P. /\ ( *Q ` x ) e. A ) <-> ( A e. P. /\ ( *Q ` ( *Q ` z ) ) e. A ) ) )
46 42 45 spcev 
 |-  ( ( A e. P. /\ ( *Q ` ( *Q ` z ) ) e. A ) -> E. x ( A e. P. /\ ( *Q ` x ) e. A ) )
47 41 46 syl6bir 
 |-  ( ( A e. P. /\ z e. A ) -> ( ( A e. P. /\ z e. A ) -> E. x ( A e. P. /\ ( *Q ` x ) e. A ) ) )
48 47 pm2.43i 
 |-  ( ( A e. P. /\ z e. A ) -> E. x ( A e. P. /\ ( *Q ` x ) e. A ) )
49 elprnq 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> ( *Q ` x ) e. Q. )
50 dmrecnq 
 |-  dom *Q = Q.
51 0nnq 
 |-  -. (/) e. Q.
52 50 51 ndmfvrcl 
 |-  ( ( *Q ` x ) e. Q. -> x e. Q. )
53 49 52 syl 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> x e. Q. )
54 ltrnq 
 |-  ( x  ( *Q ` y )
55 prcdnq 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> ( ( *Q ` y )  ( *Q ` y ) e. A ) )
56 54 55 syl5bi 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> ( x  ( *Q ` y ) e. A ) )
57 56 alrimiv 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> A. y ( x  ( *Q ` y ) e. A ) )
58 1 abeq2i 
 |-  ( x e. B <-> E. y ( x
59 exanali 
 |-  ( E. y ( x  -. A. y ( x  ( *Q ` y ) e. A ) )
60 58 59 bitri 
 |-  ( x e. B <-> -. A. y ( x  ( *Q ` y ) e. A ) )
61 60 con2bii 
 |-  ( A. y ( x  ( *Q ` y ) e. A ) <-> -. x e. B )
62 57 61 sylib 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> -. x e. B )
63 53 62 jca 
 |-  ( ( A e. P. /\ ( *Q ` x ) e. A ) -> ( x e. Q. /\ -. x e. B ) )
64 63 eximi 
 |-  ( E. x ( A e. P. /\ ( *Q ` x ) e. A ) -> E. x ( x e. Q. /\ -. x e. B ) )
65 48 64 syl 
 |-  ( ( A e. P. /\ z e. A ) -> E. x ( x e. Q. /\ -. x e. B ) )
66 65 ex 
 |-  ( A e. P. -> ( z e. A -> E. x ( x e. Q. /\ -. x e. B ) ) )
67 66 exlimdv 
 |-  ( A e. P. -> ( E. z z e. A -> E. x ( x e. Q. /\ -. x e. B ) ) )
68 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
69 nss 
 |-  ( -. Q. C_ B <-> E. x ( x e. Q. /\ -. x e. B ) )
70 67 68 69 3imtr4g 
 |-  ( A e. P. -> ( A =/= (/) -> -. Q. C_ B ) )
71 36 70 mpd 
 |-  ( A e. P. -> -. Q. C_ B )
72 ltrelnq 
 |-
73 72 brel 
 |-  ( x  ( x e. Q. /\ y e. Q. ) )
74 73 simpld 
 |-  ( x  x e. Q. )
75 74 adantr 
 |-  ( ( x  x e. Q. )
76 75 exlimiv 
 |-  ( E. y ( x  x e. Q. )
77 58 76 sylbi 
 |-  ( x e. B -> x e. Q. )
78 77 ssriv 
 |-  B C_ Q.
79 71 78 jctil 
 |-  ( A e. P. -> ( B C_ Q. /\ -. Q. C_ B ) )
80 dfpss3 
 |-  ( B C. Q. <-> ( B C_ Q. /\ -. Q. C_ B ) )
81 79 80 sylibr 
 |-  ( A e. P. -> B C. Q. )
82 35 81 jca 
 |-  ( A e. P. -> ( (/) C. B /\ B C. Q. ) )
83 ltsonq 
 |-
84 83 72 sotri 
 |-  ( ( z  z
85 84 ex 
 |-  ( z  ( x  z
86 85 anim1d 
 |-  ( z  ( ( x  ( z
87 86 eximdv 
 |-  ( z  ( E. y ( x  E. y ( z
88 87 58 24 3imtr4g 
 |-  ( z  ( x e. B -> z e. B ) )
89 88 com12 
 |-  ( x e. B -> ( z  z e. B ) )
90 89 alrimiv 
 |-  ( x e. B -> A. z ( z  z e. B ) )
91 nfe1 
 |-  F/ y E. y ( x
92 91 nfab 
 |-  F/_ y { x | E. y ( x
93 1 92 nfcxfr 
 |-  F/_ y B
94 nfv 
 |-  F/ y x
95 93 94 nfrex 
 |-  F/ y E. z e. B x
96 19.8a 
 |-  ( ( z  E. y ( z
97 96 24 sylibr 
 |-  ( ( z  z e. B )
98 97 adantll 
 |-  ( ( ( x  z e. B )
99 simpll 
 |-  ( ( ( x  x
100 98 99 jca 
 |-  ( ( ( x  ( z e. B /\ x
101 100 expcom 
 |-  ( -. ( *Q ` y ) e. A -> ( ( x  ( z e. B /\ x
102 101 eximdv 
 |-  ( -. ( *Q ` y ) e. A -> ( E. z ( x  E. z ( z e. B /\ x
103 ltbtwnnq 
 |-  ( x  E. z ( x
104 df-rex 
 |-  ( E. z e. B x  E. z ( z e. B /\ x
105 102 103 104 3imtr4g 
 |-  ( -. ( *Q ` y ) e. A -> ( x  E. z e. B x
106 105 impcom 
 |-  ( ( x  E. z e. B x
107 95 106 exlimi 
 |-  ( E. y ( x  E. z e. B x
108 58 107 sylbi 
 |-  ( x e. B -> E. z e. B x
109 90 108 jca 
 |-  ( x e. B -> ( A. z ( z  z e. B ) /\ E. z e. B x
110 109 rgen 
 |-  A. x e. B ( A. z ( z  z e. B ) /\ E. z e. B x
111 elnp 
 |-  ( B e. P. <-> ( ( (/) C. B /\ B C. Q. ) /\ A. x e. B ( A. z ( z  z e. B ) /\ E. z e. B x
112 82 110 111 sylanblrc 
 |-  ( A e. P. -> B e. P. )