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

Metamath Proof Explorer

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 } ) ) = (/) ) )