Theorem dffr7

Description: Alternate quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 26-Aug-2026)

	Ref	Expression
Assertion	dffr7	|- ( R Fr A <-> ( ~P A \ { (/) } ) C_ Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	elfix	|- ( x e. Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) <-> x ( _E o. ( _V \ ( R o. `' _E ) ) ) x )
3	1 1	coep	|- ( x ( _E o. ( _V \ ( R o. `' _E ) ) ) x <-> E. y e. x x ( _V \ ( R o. `' _E ) ) y )
4		vex	|- y e. _V
5	1 4	coepr	|- ( x ( R o. `' _E ) y <-> E. z e. x z R y )
6	5	notbii	|- ( -. x ( R o. `' _E ) y <-> -. E. z e. x z R y )
7		brv	|- x _V y
8		brdif	|- ( x ( _V \ ( R o. `' _E ) ) y <-> ( x _V y /\ -. x ( R o. `' _E ) y ) )
9	7 8	mpbiran	|- ( x ( _V \ ( R o. `' _E ) ) y <-> -. x ( R o. `' _E ) y )
10		ralnex	|- ( A. z e. x -. z R y <-> -. E. z e. x z R y )
11	6 9 10	3bitr4i	|- ( x ( _V \ ( R o. `' _E ) ) y <-> A. z e. x -. z R y )
12	11	rexbii	|- ( E. y e. x x ( _V \ ( R o. `' _E ) ) y <-> E. y e. x A. z e. x -. z R y )
13	2 3 12	3bitri	|- ( x e. Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) <-> E. y e. x A. z e. x -. z R y )
14	13	ralbii	|- ( A. x e. ( ~P A \ { (/) } ) x e. Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )
15		dfss3	|- ( ( ~P A \ { (/) } ) C_ Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) <-> A. x e. ( ~P A \ { (/) } ) x e. Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) )
16		dffr6	|- ( R Fr A <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )
17	14 15 16	3bitr4ri	|- ( R Fr A <-> ( ~P A \ { (/) } ) C_ Fix ( _E o. ( _V \ ( R o. `' _E ) ) ) )