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

Theorem fri 4687
Description: Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.)
Assertion
Ref Expression
fri  |-  ( ( ( B  e.  C  /\  R  Fr  A
)  /\  ( B  C_  A  /\  B  =/=  (/) ) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
Distinct variable groups:    x, y, A    x, B, y    x, R, y
Allowed substitution hints:    C( x, y)

Proof of Theorem fri
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-fr 4684 . . 3  |-  ( R  Fr  A  <->  A. z
( ( z  C_  A  /\  z  =/=  (/) )  ->  E. x  e.  z  A. y  e.  z  -.  y R x ) )
2 sseq1 3382 . . . . . 6  |-  ( z  =  B  ->  (
z  C_  A  <->  B  C_  A
) )
3 neeq1 2621 . . . . . 6  |-  ( z  =  B  ->  (
z  =/=  (/)  <->  B  =/=  (/) ) )
42, 3anbi12d 710 . . . . 5  |-  ( z  =  B  ->  (
( z  C_  A  /\  z  =/=  (/) )  <->  ( B  C_  A  /\  B  =/=  (/) ) ) )
5 raleq 2922 . . . . . 6  |-  ( z  =  B  ->  ( A. y  e.  z  -.  y R x  <->  A. y  e.  B  -.  y R x ) )
65rexeqbi1dv 2931 . . . . 5  |-  ( z  =  B  ->  ( E. x  e.  z  A. y  e.  z  -.  y R x  <->  E. x  e.  B  A. y  e.  B  -.  y R x ) )
74, 6imbi12d 320 . . . 4  |-  ( z  =  B  ->  (
( ( z  C_  A  /\  z  =/=  (/) )  ->  E. x  e.  z  A. y  e.  z  -.  y R x )  <-> 
( ( B  C_  A  /\  B  =/=  (/) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x ) ) )
87spcgv 3062 . . 3  |-  ( B  e.  C  ->  ( A. z ( ( z 
C_  A  /\  z  =/=  (/) )  ->  E. x  e.  z  A. y  e.  z  -.  y R x )  -> 
( ( B  C_  A  /\  B  =/=  (/) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x ) ) )
91, 8syl5bi 217 . 2  |-  ( B  e.  C  ->  ( R  Fr  A  ->  ( ( B  C_  A  /\  B  =/=  (/) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x ) ) )
109imp31 432 1  |-  ( ( ( B  e.  C  /\  R  Fr  A
)  /\  ( B  C_  A  /\  B  =/=  (/) ) )  ->  E. x  e.  B  A. y  e.  B  -.  y R x )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369   A.wal 1367    = wceq 1369    e. wcel 1756    =/= wne 2611   A.wral 2720   E.wrex 2721    C_ wss 3333   (/)c0 3642   class class class wbr 4297    Fr wfr 4681
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-v 2979  df-in 3340  df-ss 3347  df-fr 4684
This theorem is referenced by:  frc  4691  fr2nr  4703  frminex  4705  wereu  4721  wereu2  4722  fr3nr  6396  frfi  7562  fimax2g  7563  wofib  7764  wemapso  7770  wemapso2OLD  7771  wemapso2lem  7772  noinfep  7870  noinfepOLD  7871  cflim2  8437  isfin1-3  8560  fin12  8587  fpwwe2lem12  8813  fpwwe2lem13  8814  fpwwe2  8815  frinfm  28634  fdc  28646  fnwe2lem2  29409  bnj110  31856
  Copyright terms: Public domain W3C validator