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

Theorem fri 4828
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 4825 . . 3  |-  ( R  Fr  A  <->  A. z
( ( z  C_  A  /\  z  =/=  (/) )  ->  E. x  e.  z  A. y  e.  z  -.  y R x ) )
2 sseq1 3508 . . . . . 6  |-  ( z  =  B  ->  (
z  C_  A  <->  B  C_  A
) )
3 neeq1 2722 . . . . . 6  |-  ( z  =  B  ->  (
z  =/=  (/)  <->  B  =/=  (/) ) )
42, 3anbi12d 710 . . . . 5  |-  ( z  =  B  ->  (
( z  C_  A  /\  z  =/=  (/) )  <->  ( B  C_  A  /\  B  =/=  (/) ) ) )
5 raleq 3038 . . . . . 6  |-  ( z  =  B  ->  ( A. y  e.  z  -.  y R x  <->  A. y  e.  B  -.  y R x ) )
65rexeqbi1dv 3047 . . . . 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 3178 . . 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 1379    = wceq 1381    e. wcel 1802    =/= wne 2636   A.wral 2791   E.wrex 2792    C_ wss 3459   (/)c0 3768   class class class wbr 4434    Fr wfr 4822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-v 3095  df-in 3466  df-ss 3473  df-fr 4825
This theorem is referenced by:  frc  4832  fr2nr  4844  frminex  4846  wereu  4862  wereu2  4863  fr3nr  6597  frfi  7764  fimax2g  7765  wofib  7970  wemapso  7976  wemapso2OLD  7977  wemapso2lem  7978  noinfep  8076  noinfepOLD  8077  cflim2  8643  isfin1-3  8766  fin12  8793  fpwwe2lem12  9019  fpwwe2lem13  9020  fpwwe2  9021  frinfm  30198  fdc  30210  fnwe2lem2  30969  bnj110  33644
  Copyright terms: Public domain W3C validator