Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Founded and well-ordering relations
dffr2
Metamath Proof Explorer
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 } = (/) ) )