This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion dffr4 
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 dffr3 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
2 df-pred 
 |-  Pred ( R , x , y ) = ( x i^i ( `' R " { y } ) )
3 2 eqeq1i 
 |-  ( Pred ( R , x , y ) = (/) <-> ( x i^i ( `' R " { y } ) ) = (/) )
4 3 rexbii 
 |-  ( E. y e. x Pred ( R , x , y ) = (/) <-> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) )
5 4 imbi2i 
 |-  ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
6 5 albii 
 |-  ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )
7 1 6 bitr4i 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x Pred ( R , x , y ) = (/) ) )