Theorem dffr3

Description: Alternate definition of well-founded relation. Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 23-Jun-2015)

	Ref	Expression
Assertion	dffr3	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		dffr2	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )
2		iniseg	|- ( y e. _V -> ( `' R " { y } ) = { z | z R y } )
3	2	elv	|- ( `' R " { y } ) = { z | z R y }
4	3	ineq2i	|- ( x i^i ( `' R " { y } ) ) = ( x i^i { z | z R y } )
5		dfrab3	|- { z e. x | z R y } = ( x i^i { z | z R y } )
6	4 5	eqtr4i	|- ( x i^i ( `' R " { y } ) ) = { z e. x | z R y }
7	6	eqeq1i	|- ( ( x i^i ( `' R " { y } ) ) = (/) <-> { z e. x | z R y } = (/) )
8	7	rexbii	|- ( E. y e. x ( x i^i ( `' R " { y } ) ) = (/) <-> E. y e. x { z e. x | z R y } = (/) )
9	8	imbi2i	|- ( ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )
10	9	albii	|- ( A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x { z e. x | z R y } = (/) ) )
11	1 10	bitr4i	|- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x ( x i^i ( `' R " { y } ) ) = (/) ) )