Metamath Proof Explorer


Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015) Avoid ax-10 , ax-11 , ax-12 , but use ax-8 . (Revised by Gino Giotto, 3-Oct-2024)

Ref Expression
Assertion dffr2
|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )

Proof

Step Hyp Ref Expression
1 df-fr
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. w e. x -. w R y ) )
2 breq1
 |-  ( z = w -> ( z R y <-> w R y ) )
3 2 rabeq0w
 |-  ( { z e. x | z R y } = (/) <-> A. w e. x -. w R y )
4 3 rexbii
 |-  ( E. y e. x { z e. x | z R y } = (/) <-> E. y e. x A. w e. x -. w R y )
5 4 imbi2i
 |-  ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. w e. x -. w R y ) )
6 5 albii
 |-  ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. w e. x -. w R y ) )
7 1 6 bitr4i
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )