Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1417 Structured version   Visualization version   Unicode version

Theorem bnj1417 29850
Description: Technical lemma for bnj60 29871. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Mario Carneiro, 22-Dec-2016.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1417.1  |-  ( ph  <->  R 
FrSe  A )
bnj1417.2  |-  ( ps  <->  -.  x  e.  trCl (
x ,  A ,  R ) )
bnj1417.3  |-  ( ch  <->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ps ) )
bnj1417.4  |-  ( th  <->  (
ph  /\  x  e.  A  /\  ch ) )
bnj1417.5  |-  B  =  (  pred ( x ,  A ,  R )  u.  U_ y  e. 
pred  ( x ,  A ,  R ) 
trCl ( y ,  A ,  R ) )
Assertion
Ref Expression
bnj1417  |-  ( ph  ->  A. x  e.  A  -.  x  e.  trCl ( x ,  A ,  R ) )
Distinct variable groups:    x, A, y    x, R, y    ph, x, y    ps, y
Allowed substitution hints:    ps( x)    ch( x, y)    th( x, y)    B( x, y)

Proof of Theorem bnj1417
StepHypRef Expression
1 bnj1417.1 . . . 4  |-  ( ph  <->  R 
FrSe  A )
21biimpi 198 . . 3  |-  ( ph  ->  R  FrSe  A )
3 bnj1417.4 . . . . . 6  |-  ( th  <->  (
ph  /\  x  e.  A  /\  ch ) )
4 bnj1418 29849 . . . . . . . . . . 11  |-  ( x  e.  pred ( x ,  A ,  R )  ->  x R x )
54adantl 468 . . . . . . . . . 10  |-  ( ( th  /\  x  e. 
pred ( x ,  A ,  R ) )  ->  x R x )
63, 2bnj835 29570 . . . . . . . . . . . 12  |-  ( th 
->  R  FrSe  A )
7 df-bnj15 29498 . . . . . . . . . . . . 13  |-  ( R 
FrSe  A  <->  ( R  Fr  A  /\  R  Se  A
) )
87simplbi 462 . . . . . . . . . . . 12  |-  ( R 
FrSe  A  ->  R  Fr  A )
96, 8syl 17 . . . . . . . . . . 11  |-  ( th 
->  R  Fr  A
)
10 bnj213 29693 . . . . . . . . . . . 12  |-  pred (
x ,  A ,  R )  C_  A
1110sseli 3428 . . . . . . . . . . 11  |-  ( x  e.  pred ( x ,  A ,  R )  ->  x  e.  A
)
12 frirr 4811 . . . . . . . . . . 11  |-  ( ( R  Fr  A  /\  x  e.  A )  ->  -.  x R x )
139, 11, 12syl2an 480 . . . . . . . . . 10  |-  ( ( th  /\  x  e. 
pred ( x ,  A ,  R ) )  ->  -.  x R x )
145, 13pm2.65da 580 . . . . . . . . 9  |-  ( th 
->  -.  x  e.  pred ( x ,  A ,  R ) )
15 nfv 1761 . . . . . . . . . . . . . 14  |-  F/ y
ph
16 nfv 1761 . . . . . . . . . . . . . 14  |-  F/ y  x  e.  A
17 bnj1417.3 . . . . . . . . . . . . . . . 16  |-  ( ch  <->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ps ) )
1817bnj1095 29593 . . . . . . . . . . . . . . 15  |-  ( ch 
->  A. y ch )
1918nfi 1674 . . . . . . . . . . . . . 14  |-  F/ y ch
2015, 16, 19nf3an 2013 . . . . . . . . . . . . 13  |-  F/ y ( ph  /\  x  e.  A  /\  ch )
213, 20nfxfr 1696 . . . . . . . . . . . 12  |-  F/ y th
226ad2antrr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  R  FrSe  A )
23 simplr 762 . . . . . . . . . . . . . . . . 17  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  y  e.  pred ( x ,  A ,  R ) )
2410, 23sseldi 3430 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  y  e.  A )
25 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  x  e.  trCl ( y ,  A ,  R ) )
26 bnj1125 29801 . . . . . . . . . . . . . . . 16  |-  ( ( R  FrSe  A  /\  y  e.  A  /\  x  e.  trCl ( y ,  A ,  R
) )  ->  trCl (
x ,  A ,  R )  C_  trCl (
y ,  A ,  R ) )
2722, 24, 25, 26syl3anc 1268 . . . . . . . . . . . . . . 15  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  trCl ( x ,  A ,  R
)  C_  trCl ( y ,  A ,  R
) )
28 bnj1147 29803 . . . . . . . . . . . . . . . . . 18  |-  trCl (
y ,  A ,  R )  C_  A
2928, 25sseldi 3430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  x  e.  A )
30 bnj906 29741 . . . . . . . . . . . . . . . . 17  |-  ( ( R  FrSe  A  /\  x  e.  A )  ->  pred ( x ,  A ,  R ) 
C_  trCl ( x ,  A ,  R ) )
3122, 29, 30syl2anc 667 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  pred ( x ,  A ,  R
)  C_  trCl ( x ,  A ,  R
) )
3231, 23sseldd 3433 . . . . . . . . . . . . . . 15  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  y  e.  trCl ( x ,  A ,  R ) )
3327, 32sseldd 3433 . . . . . . . . . . . . . 14  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  y  e.  trCl ( y ,  A ,  R ) )
3417biimpi 198 . . . . . . . . . . . . . . . . . 18  |-  ( ch 
->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ps ) )
353, 34bnj837 29572 . . . . . . . . . . . . . . . . 17  |-  ( th 
->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ps ) )
3635ad2antrr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  A. y  e.  A  ( y R x  ->  [. y  /  x ]. ps )
)
37 bnj1418 29849 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  pred ( x ,  A ,  R )  ->  y R x )
3837ad2antlr 733 . . . . . . . . . . . . . . . 16  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  y R x )
39 rsp 2754 . . . . . . . . . . . . . . . 16  |-  ( A. y  e.  A  (
y R x  ->  [. y  /  x ]. ps )  ->  (
y  e.  A  -> 
( y R x  ->  [. y  /  x ]. ps ) ) )
4036, 24, 38, 39syl3c 63 . . . . . . . . . . . . . . 15  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  [. y  /  x ]. ps )
41 vex 3048 . . . . . . . . . . . . . . . 16  |-  y  e. 
_V
42 bnj1417.2 . . . . . . . . . . . . . . . . 17  |-  ( ps  <->  -.  x  e.  trCl (
x ,  A ,  R ) )
43 eleq1 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
x  e.  trCl (
x ,  A ,  R )  <->  y  e.  trCl ( x ,  A ,  R ) ) )
44 bnj1318 29834 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  trCl (
x ,  A ,  R )  =  trCl ( y ,  A ,  R ) )
4544eleq2d 2514 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
y  e.  trCl (
x ,  A ,  R )  <->  y  e.  trCl ( y ,  A ,  R ) ) )
4643, 45bitrd 257 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  y  ->  (
x  e.  trCl (
x ,  A ,  R )  <->  y  e.  trCl ( y ,  A ,  R ) ) )
4746notbid 296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  y  ->  ( -.  x  e.  trCl ( x ,  A ,  R )  <->  -.  y  e.  trCl ( y ,  A ,  R ) ) )
4842, 47syl5bb 261 . . . . . . . . . . . . . . . 16  |-  ( x  =  y  ->  ( ps 
<->  -.  y  e.  trCl ( y ,  A ,  R ) ) )
4941, 48sbcie 3302 . . . . . . . . . . . . . . 15  |-  ( [. y  /  x ]. ps  <->  -.  y  e.  trCl (
y ,  A ,  R ) )
5040, 49sylib 200 . . . . . . . . . . . . . 14  |-  ( ( ( th  /\  y  e.  pred ( x ,  A ,  R ) )  /\  x  e. 
trCl ( y ,  A ,  R ) )  ->  -.  y  e.  trCl ( y ,  A ,  R ) )
5133, 50pm2.65da 580 . . . . . . . . . . . . 13  |-  ( ( th  /\  y  e. 
pred ( x ,  A ,  R ) )  ->  -.  x  e.  trCl ( y ,  A ,  R ) )
5251ex 436 . . . . . . . . . . . 12  |-  ( th 
->  ( y  e.  pred ( x ,  A ,  R )  ->  -.  x  e.  trCl ( y ,  A ,  R
) ) )
5321, 52ralrimi 2788 . . . . . . . . . . 11  |-  ( th 
->  A. y  e.  pred  ( x ,  A ,  R )  -.  x  e.  trCl ( y ,  A ,  R ) )
54 ralnex 2834 . . . . . . . . . . 11  |-  ( A. y  e.  pred  ( x ,  A ,  R
)  -.  x  e. 
trCl ( y ,  A ,  R )  <->  -.  E. y  e.  pred  ( x ,  A ,  R ) x  e. 
trCl ( y ,  A ,  R ) )
5553, 54sylib 200 . . . . . . . . . 10  |-  ( th 
->  -.  E. y  e. 
pred  ( x ,  A ,  R ) x  e.  trCl (
y ,  A ,  R ) )
56 eliun 4283 . . . . . . . . . 10  |-  ( x  e.  U_ y  e. 
pred  ( x ,  A ,  R ) 
trCl ( y ,  A ,  R )  <->  E. y  e.  pred  ( x ,  A ,  R ) x  e. 
trCl ( y ,  A ,  R ) )
5755, 56sylnibr 307 . . . . . . . . 9  |-  ( th 
->  -.  x  e.  U_ y  e.  pred  ( x ,  A ,  R
)  trCl ( y ,  A ,  R ) )
58 ioran 493 . . . . . . . . 9  |-  ( -.  ( x  e.  pred ( x ,  A ,  R )  \/  x  e.  U_ y  e.  pred  ( x ,  A ,  R )  trCl (
y ,  A ,  R ) )  <->  ( -.  x  e.  pred ( x ,  A ,  R
)  /\  -.  x  e.  U_ y  e.  pred  ( x ,  A ,  R )  trCl (
y ,  A ,  R ) ) )
5914, 57, 58sylanbrc 670 . . . . . . . 8  |-  ( th 
->  -.  ( x  e. 
pred ( x ,  A ,  R )  \/  x  e.  U_ y  e.  pred  ( x ,  A ,  R
)  trCl ( y ,  A ,  R ) ) )
603simp2bi 1024 . . . . . . . . . . 11  |-  ( th 
->  x  e.  A
)
61 bnj1417.5 . . . . . . . . . . . 12  |-  B  =  (  pred ( x ,  A ,  R )  u.  U_ y  e. 
pred  ( x ,  A ,  R ) 
trCl ( y ,  A ,  R ) )
6261bnj1414 29846 . . . . . . . . . . 11  |-  ( ( R  FrSe  A  /\  x  e.  A )  ->  trCl ( x ,  A ,  R )  =  B )
636, 60, 62syl2anc 667 . . . . . . . . . 10  |-  ( th 
->  trCl ( x ,  A ,  R )  =  B )
6463eleq2d 2514 . . . . . . . . 9  |-  ( th 
->  ( x  e.  trCl ( x ,  A ,  R )  <->  x  e.  B ) )
6561bnj1138 29600 . . . . . . . . 9  |-  ( x  e.  B  <->  ( x  e.  pred ( x ,  A ,  R )  \/  x  e.  U_ y  e.  pred  ( x ,  A ,  R
)  trCl ( y ,  A ,  R ) ) )
6664, 65syl6bb 265 . . . . . . . 8  |-  ( th 
->  ( x  e.  trCl ( x ,  A ,  R )  <->  ( x  e.  pred ( x ,  A ,  R )  \/  x  e.  U_ y  e.  pred  ( x ,  A ,  R
)  trCl ( y ,  A ,  R ) ) ) )
6759, 66mtbird 303 . . . . . . 7  |-  ( th 
->  -.  x  e.  trCl ( x ,  A ,  R ) )
6867, 42sylibr 216 . . . . . 6  |-  ( th 
->  ps )
693, 68sylbir 217 . . . . 5  |-  ( (
ph  /\  x  e.  A  /\  ch )  ->  ps )
70693exp 1207 . . . 4  |-  ( ph  ->  ( x  e.  A  ->  ( ch  ->  ps ) ) )
7170ralrimiv 2800 . . 3  |-  ( ph  ->  A. x  e.  A  ( ch  ->  ps )
)
7217bnj1204 29821 . . 3  |-  ( ( R  FrSe  A  /\  A. x  e.  A  ( ch  ->  ps )
)  ->  A. x  e.  A  ps )
732, 71, 72syl2anc 667 . 2  |-  ( ph  ->  A. x  e.  A  ps )
7442ralbii 2819 . 2  |-  ( A. x  e.  A  ps  <->  A. x  e.  A  -.  x  e.  trCl ( x ,  A ,  R
) )
7573, 74sylib 200 1  |-  ( ph  ->  A. x  e.  A  -.  x  e.  trCl ( x ,  A ,  R ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    /\ w3a 985    = wceq 1444    e. wcel 1887   A.wral 2737   E.wrex 2738   [.wsbc 3267    u. cun 3402    C_ wss 3404   U_ciun 4278   class class class wbr 4402    Fr wfr 4790    predc-bnj14 29493    Se w-bnj13 29495    FrSe w-bnj15 29497    trClc-bnj18 29499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-reg 8107  ax-inf2 8146
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-fal 1450  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-om 6693  df-1o 7182  df-bnj17 29492  df-bnj14 29494  df-bnj13 29496  df-bnj15 29498  df-bnj18 29500  df-bnj19 29502
This theorem is referenced by:  bnj1421  29851
  Copyright terms: Public domain W3C validator