Metamath Proof Explorer

Theorem dffr5

Description: A quantifier-free definition of a well-founded relation. (Contributed by Scott Fenton, 11-Apr-2011) (Proof shortened by Scott Fenton, 26-Aug-2026)

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

Proof

Step Hyp Ref Expression
1 brdif 
 |-  ( y ( _E \ ( _E o. `' R ) ) x <-> ( y _E x /\ -. y ( _E o. `' R ) x ) )
2 epel 
 |-  ( y _E x <-> y e. x )
3 vex 
 |-  y e. _V
4 vex 
 |-  x e. _V
5 3 4 coep 
 |-  ( y ( _E o. `' R ) x <-> E. z e. x y `' R z )
6 vex 
 |-  z e. _V
7 3 6 brcnv 
 |-  ( y `' R z <-> z R y )
8 7 rexbii 
 |-  ( E. z e. x y `' R z <-> E. z e. x z R y )
9 dfrex2 
 |-  ( E. z e. x z R y <-> -. A. z e. x -. z R y )
10 5 8 9 3bitrri 
 |-  ( -. A. z e. x -. z R y <-> y ( _E o. `' R ) x )
11 10 con1bii 
 |-  ( -. y ( _E o. `' R ) x <-> A. z e. x -. z R y )
12 2 11 anbi12i 
 |-  ( ( y _E x /\ -. y ( _E o. `' R ) x ) <-> ( y e. x /\ A. z e. x -. z R y ) )
13 1 12 bitri 
 |-  ( y ( _E \ ( _E o. `' R ) ) x <-> ( y e. x /\ A. z e. x -. z R y ) )
14 13 exbii 
 |-  ( E. y y ( _E \ ( _E o. `' R ) ) x <-> E. y ( y e. x /\ A. z e. x -. z R y ) )
15 4 elrn 
 |-  ( x e. ran ( _E \ ( _E o. `' R ) ) <-> E. y y ( _E \ ( _E o. `' R ) ) x )
16 df-rex 
 |-  ( E. y e. x A. z e. x -. z R y <-> E. y ( y e. x /\ A. z e. x -. z R y ) )
17 14 15 16 3bitr4i 
 |-  ( x e. ran ( _E \ ( _E o. `' R ) ) <-> E. y e. x A. z e. x -. z R y )
18 17 ralbii 
 |-  ( A. x e. ( ~P A \ { (/) } ) x e. ran ( _E \ ( _E o. `' R ) ) <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )
19 dfss3 
 |-  ( ( ~P A \ { (/) } ) C_ ran ( _E \ ( _E o. `' R ) ) <-> A. x e. ( ~P A \ { (/) } ) x e. ran ( _E \ ( _E o. `' R ) ) )
20 dffr6 
 |-  ( R Fr A <-> A. x e. ( ~P A \ { (/) } ) E. y e. x A. z e. x -. z R y )
21 18 19 20 3bitr4ri 
 |-  ( R Fr A <-> ( ~P A \ { (/) } ) C_ ran ( _E \ ( _E o. `' R ) ) )