Metamath Proof Explorer

Theorem fri

Description: Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997)

Ref Expression
Assertion fri 
|- ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )

Proof

Step Hyp Ref Expression
1 df-fr 
 |-  ( R Fr A <-> A. z ( ( z C_ A /\ z =/= (/) ) -> E. x e. z A. y e. z -. y R x ) )
2 sseq1 
 |-  ( z = B -> ( z C_ A <-> B C_ A ) )
3 neeq1 
 |-  ( z = B -> ( z =/= (/) <-> B =/= (/) ) )
4 2 3 anbi12d 
 |-  ( z = B -> ( ( z C_ A /\ z =/= (/) ) <-> ( B C_ A /\ B =/= (/) ) ) )
5 raleq 
 |-  ( z = B -> ( A. y e. z -. y R x <-> A. y e. B -. y R x ) )
6 5 rexeqbi1dv 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( B e. C -> ( R Fr A -> ( ( B C_ A /\ B =/= (/) ) -> E. x e. B A. y e. B -. y R x ) ) )
10 9 imp31 
 |-  ( ( ( B e. C /\ R Fr A ) /\ ( B C_ A /\ B =/= (/) ) ) -> E. x e. B A. y e. B -. y R x )