MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reclem4pr Structured version   Unicode version

Theorem reclem4pr 9361
Description: Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.)
Hypothesis
Ref Expression
reclempr.1  |-  B  =  { x  |  E. y ( x  <Q  y  /\  -.  ( *Q
`  y )  e.  A ) }
Assertion
Ref Expression
reclem4pr  |-  ( A  e.  P.  ->  ( A  .P.  B )  =  1P )
Distinct variable groups:    x, y, A    x, B
Allowed substitution hint:    B( y)

Proof of Theorem reclem4pr
Dummy variables  z  w  u  f  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reclempr.1 . . . . . . 7  |-  B  =  { x  |  E. y ( x  <Q  y  /\  -.  ( *Q
`  y )  e.  A ) }
21reclem2pr 9359 . . . . . 6  |-  ( A  e.  P.  ->  B  e.  P. )
3 df-mp 9295 . . . . . . 7  |-  .P.  =  ( y  e.  P. ,  w  e.  P.  |->  { u  |  E. f  e.  y  E. g  e.  w  u  =  ( f  .Q  g ) } )
4 mulclnq 9258 . . . . . . 7  |-  ( ( f  e.  Q.  /\  g  e.  Q. )  ->  ( f  .Q  g
)  e.  Q. )
53, 4genpelv 9311 . . . . . 6  |-  ( ( A  e.  P.  /\  B  e.  P. )  ->  ( w  e.  ( A  .P.  B )  <->  E. z  e.  A  E. x  e.  B  w  =  ( z  .Q  x ) ) )
62, 5mpdan 666 . . . . 5  |-  ( A  e.  P.  ->  (
w  e.  ( A  .P.  B )  <->  E. z  e.  A  E. x  e.  B  w  =  ( z  .Q  x
) ) )
71abeq2i 2523 . . . . . . . . 9  |-  ( x  e.  B  <->  E. y
( x  <Q  y  /\  -.  ( *Q `  y )  e.  A
) )
8 ltrelnq 9237 . . . . . . . . . . . . . . 15  |-  <Q  C_  ( Q.  X.  Q. )
98brel 4979 . . . . . . . . . . . . . 14  |-  ( x 
<Q  y  ->  ( x  e.  Q.  /\  y  e.  Q. ) )
109simprd 461 . . . . . . . . . . . . 13  |-  ( x 
<Q  y  ->  y  e. 
Q. )
11 elprnq 9302 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  z  e.  Q. )
12 ltmnq 9283 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  Q.  ->  (
x  <Q  y  <->  ( z  .Q  x )  <Q  (
z  .Q  y ) ) )
1311, 12syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  <Q  y  <->  ( z  .Q  x ) 
<Q  ( z  .Q  y
) ) )
1413biimpd 207 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  <Q  y  ->  ( z  .Q  x
)  <Q  ( z  .Q  y ) ) )
1514adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( x  <Q  y  ->  ( z  .Q  x )  <Q  (
z  .Q  y ) ) )
16 recclnq 9277 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  Q.  ->  ( *Q `  y )  e. 
Q. )
17 prub 9305 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  ( *Q `  y )  e.  Q. )  ->  ( -.  ( *Q `  y )  e.  A  ->  z  <Q  ( *Q `  y ) ) )
1816, 17sylan2 472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( -.  ( *Q `  y )  e.  A  ->  z  <Q  ( *Q `  y ) ) )
19 ltmnq 9283 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  Q.  ->  (
z  <Q  ( *Q `  y )  <->  ( y  .Q  z )  <Q  (
y  .Q  ( *Q
`  y ) ) ) )
20 mulcomnq 9264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  .Q  z )  =  ( z  .Q  y
)
2120a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  Q.  ->  (
y  .Q  z )  =  ( z  .Q  y ) )
22 recidnq 9276 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  Q.  ->  (
y  .Q  ( *Q
`  y ) )  =  1Q )
2321, 22breq12d 4397 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  Q.  ->  (
( y  .Q  z
)  <Q  ( y  .Q  ( *Q `  y
) )  <->  ( z  .Q  y )  <Q  1Q ) )
2419, 23bitrd 253 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  Q.  ->  (
z  <Q  ( *Q `  y )  <->  ( z  .Q  y )  <Q  1Q ) )
2524adantl 464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( z  <Q 
( *Q `  y
)  <->  ( z  .Q  y )  <Q  1Q ) )
2618, 25sylibd 214 . . . . . . . . . . . . . . . 16  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( -.  ( *Q `  y )  e.  A  ->  ( z  .Q  y )  <Q  1Q ) )
2715, 26anim12d 561 . . . . . . . . . . . . . . 15  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( ( x 
<Q  y  /\  -.  ( *Q `  y )  e.  A )  ->  (
( z  .Q  x
)  <Q  ( z  .Q  y )  /\  (
z  .Q  y ) 
<Q  1Q ) ) )
28 ltsonq 9280 . . . . . . . . . . . . . . . 16  |-  <Q  Or  Q.
2928, 8sotri 5324 . . . . . . . . . . . . . . 15  |-  ( ( ( z  .Q  x
)  <Q  ( z  .Q  y )  /\  (
z  .Q  y ) 
<Q  1Q )  ->  (
z  .Q  x ) 
<Q  1Q )
3027, 29syl6 33 . . . . . . . . . . . . . 14  |-  ( ( ( A  e.  P.  /\  z  e.  A )  /\  y  e.  Q. )  ->  ( ( x 
<Q  y  /\  -.  ( *Q `  y )  e.  A )  ->  (
z  .Q  x ) 
<Q  1Q ) )
3130exp4b 605 . . . . . . . . . . . . 13  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( y  e.  Q.  ->  ( x  <Q  y  ->  ( -.  ( *Q
`  y )  e.  A  ->  ( z  .Q  x )  <Q  1Q ) ) ) )
3210, 31syl5 32 . . . . . . . . . . . 12  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  <Q  y  ->  ( x  <Q  y  ->  ( -.  ( *Q
`  y )  e.  A  ->  ( z  .Q  x )  <Q  1Q ) ) ) )
3332pm2.43d 48 . . . . . . . . . . 11  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  <Q  y  ->  ( -.  ( *Q
`  y )  e.  A  ->  ( z  .Q  x )  <Q  1Q ) ) )
3433impd 429 . . . . . . . . . 10  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( ( x  <Q  y  /\  -.  ( *Q
`  y )  e.  A )  ->  (
z  .Q  x ) 
<Q  1Q ) )
3534exlimdv 1739 . . . . . . . . 9  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( E. y ( x  <Q  y  /\  -.  ( *Q `  y
)  e.  A )  ->  ( z  .Q  x )  <Q  1Q ) )
367, 35syl5bi 217 . . . . . . . 8  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  e.  B  ->  ( z  .Q  x
)  <Q  1Q ) )
37 breq1 4387 . . . . . . . . 9  |-  ( w  =  ( z  .Q  x )  ->  (
w  <Q  1Q  <->  ( z  .Q  x )  <Q  1Q ) )
3837biimprcd 225 . . . . . . . 8  |-  ( ( z  .Q  x ) 
<Q  1Q  ->  ( w  =  ( z  .Q  x )  ->  w  <Q  1Q ) )
3936, 38syl6 33 . . . . . . 7  |-  ( ( A  e.  P.  /\  z  e.  A )  ->  ( x  e.  B  ->  ( w  =  ( z  .Q  x )  ->  w  <Q  1Q ) ) )
4039expimpd 601 . . . . . 6  |-  ( A  e.  P.  ->  (
( z  e.  A  /\  x  e.  B
)  ->  ( w  =  ( z  .Q  x )  ->  w  <Q  1Q ) ) )
4140rexlimdvv 2894 . . . . 5  |-  ( A  e.  P.  ->  ( E. z  e.  A  E. x  e.  B  w  =  ( z  .Q  x )  ->  w  <Q  1Q ) )
426, 41sylbid 215 . . . 4  |-  ( A  e.  P.  ->  (
w  e.  ( A  .P.  B )  ->  w  <Q  1Q ) )
43 df-1p 9293 . . . . 5  |-  1P  =  { w  |  w  <Q  1Q }
4443abeq2i 2523 . . . 4  |-  ( w  e.  1P  <->  w  <Q  1Q )
4542, 44syl6ibr 227 . . 3  |-  ( A  e.  P.  ->  (
w  e.  ( A  .P.  B )  ->  w  e.  1P )
)
4645ssrdv 3440 . 2  |-  ( A  e.  P.  ->  ( A  .P.  B )  C_  1P )
471reclem3pr 9360 . 2  |-  ( A  e.  P.  ->  1P  C_  ( A  .P.  B
) )
4846, 47eqssd 3451 1  |-  ( A  e.  P.  ->  ( A  .P.  B )  =  1P )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399   E.wex 1627    e. wcel 1836   {cab 2381   E.wrex 2747   class class class wbr 4384   ` cfv 5513  (class class class)co 6218   Q.cnq 9163   1Qc1q 9164    .Q cmq 9167   *Qcrq 9168    <Q cltq 9169   P.cnp 9170   1Pc1p 9171    .P. cmp 9173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-inf2 7994
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-int 4217  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-1o 7070  df-oadd 7074  df-omul 7075  df-er 7251  df-ni 9183  df-pli 9184  df-mi 9185  df-lti 9186  df-plpq 9219  df-mpq 9220  df-ltpq 9221  df-enq 9222  df-nq 9223  df-erq 9224  df-plq 9225  df-mq 9226  df-1nq 9227  df-rq 9228  df-ltnq 9229  df-np 9292  df-1p 9293  df-mp 9295
This theorem is referenced by:  recexpr  9362
  Copyright terms: Public domain W3C validator