Metamath Proof Explorer

Theorem dffr5

Description: A quantifier-free definition of a well-founded relationship. (Contributed by Scott Fenton, 11-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( x e. ( ~P A \ { (/) } ) <-> ( x e. ~P A /\ -. x e. { (/) } ) )
2 velpw 
 |-  ( x e. ~P A <-> x C_ A )
3 velsn 
 |-  ( x e. { (/) } <-> x = (/) )
4 3 necon3bbii 
 |-  ( -. x e. { (/) } <-> x =/= (/) )
5 2 4 anbi12i 
 |-  ( ( x e. ~P A /\ -. x e. { (/) } ) <-> ( x C_ A /\ x =/= (/) ) )
6 1 5 bitri 
 |-  ( x e. ( ~P A \ { (/) } ) <-> ( x C_ A /\ x =/= (/) ) )
7 brdif 
 |-  ( y ( _E \ ( _E o. `' R ) ) x <-> ( y _E x /\ -. y ( _E o. `' R ) x ) )
8 epel 
 |-  ( y _E x <-> y e. x )
9 vex 
 |-  y e. _V
10 vex 
 |-  x e. _V
11 9 10 coep 
 |-  ( y ( _E o. `' R ) x <-> E. z e. x y `' R z )
12 vex 
 |-  z e. _V
13 9 12 brcnv 
 |-  ( y `' R z <-> z R y )
14 13 rexbii 
 |-  ( E. z e. x y `' R z <-> E. z e. x z R y )
15 dfrex2 
 |-  ( E. z e. x z R y <-> -. A. z e. x -. z R y )
16 11 14 15 3bitrri 
 |-  ( -. A. z e. x -. z R y <-> y ( _E o. `' R ) x )
17 16 con1bii 
 |-  ( -. y ( _E o. `' R ) x <-> A. z e. x -. z R y )
18 8 17 anbi12i 
 |-  ( ( y _E x /\ -. y ( _E o. `' R ) x ) <-> ( y e. x /\ A. z e. x -. z R y ) )
19 7 18 bitri 
 |-  ( y ( _E \ ( _E o. `' R ) ) x <-> ( y e. x /\ A. z e. x -. z R y ) )
20 19 exbii 
 |-  ( E. y y ( _E \ ( _E o. `' R ) ) x <-> E. y ( y e. x /\ A. z e. x -. z R y ) )
21 10 elrn 
 |-  ( x e. ran ( _E \ ( _E o. `' R ) ) <-> E. y y ( _E \ ( _E o. `' R ) ) x )
22 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 ) )
23 20 21 22 3bitr4i 
 |-  ( x e. ran ( _E \ ( _E o. `' R ) ) <-> E. y e. x A. z e. x -. z R y )
24 6 23 imbi12i 
 |-  ( ( x e. ( ~P A \ { (/) } ) -> x e. ran ( _E \ ( _E o. `' R ) ) ) <-> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
25 24 albii 
 |-  ( A. x ( x e. ( ~P A \ { (/) } ) -> x e. ran ( _E \ ( _E o. `' R ) ) ) <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
26 dfss2 
 |-  ( ( ~P A \ { (/) } ) C_ ran ( _E \ ( _E o. `' R ) ) <-> A. x ( x e. ( ~P A \ { (/) } ) -> x e. ran ( _E \ ( _E o. `' R ) ) ) )
27 df-fr 
 |-  ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
28 25 26 27 3bitr4ri 
 |-  ( R Fr A <-> ( ~P A \ { (/) } ) C_ ran ( _E \ ( _E o. `' R ) ) )