Theorem fri 5076

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.

Step	Hyp	Ref	Expression
1		df-fr 5073	. . 3 |- ( R Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) )
2		sseq1 3626	. . . . . 6 |- ( z = B -> ( z C_ A <-> B C_ A ) )
3		neeq1 2856	. . . . . 6 |- ( z = B -> ( z =/= (/) <-> B =/= (/) ) )
4	2, 3	anbi12d 747	. . . . 5 |- ( z = B -> ( ( z C_ A /\ z =/= (/) ) <-> ( B C_ A /\ B =/= (/) ) ) )
5		raleq 3138	. . . . . 6 |- ( z = B -> ( A. y e. z -. y R x <-> A. y e. B -. y R x ) )
6	5	rexeqbi1dv 3147	. . . . 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 ) )
7	4, 6	imbi12d 334	. . . 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 ) ) )
8	7	spcgv 3293	. . 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 ) ) )
9	1, 8	syl5bi 232	. 2 |- ( B e. C -> ( R Fr A -> ( ( B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
10	9	imp31 448	1 |- ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   A.wal 1481   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   C_ wss 3574   (/)c0 3915   class class class wbr 4653   Fr wfr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-fr 5073

This theorem is referenced by:  frc  5080  fr2nr  5092  frminex  5094  wereu  5110  wereu2  5111  fr3nr  6979  frfi  8205  fimax2g  8206  fimin2g  8403  wofib  8450  wemapso  8456  wemapso2lem  8457  noinfep  8557  cflim2  9085  isfin1-3  9208  fin12  9235  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  bnj110  30928  frinfm  33530  fdc  33541  fnwe2lem2  37621