This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Founded and well-ordering relations 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 GG , 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 } = (/) ) )