Step |
Hyp |
Ref |
Expression |
1 |
|
df-he |
|- ( R hereditary A <-> ( R " A ) C_ A ) |
2 |
|
19.21v |
|- ( A. y ( x e. A -> ( x R y -> y e. A ) ) <-> ( x e. A -> A. y ( x R y -> y e. A ) ) ) |
3 |
2
|
bicomi |
|- ( ( x e. A -> A. y ( x R y -> y e. A ) ) <-> A. y ( x e. A -> ( x R y -> y e. A ) ) ) |
4 |
3
|
albii |
|- ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> A. x A. y ( x e. A -> ( x R y -> y e. A ) ) ) |
5 |
|
alcom |
|- ( A. x A. y ( x e. A -> ( x R y -> y e. A ) ) <-> A. y A. x ( x e. A -> ( x R y -> y e. A ) ) ) |
6 |
|
impexp |
|- ( ( ( x e. A /\ x R y ) -> y e. A ) <-> ( x e. A -> ( x R y -> y e. A ) ) ) |
7 |
6
|
bicomi |
|- ( ( x e. A -> ( x R y -> y e. A ) ) <-> ( ( x e. A /\ x R y ) -> y e. A ) ) |
8 |
7
|
albii |
|- ( A. x ( x e. A -> ( x R y -> y e. A ) ) <-> A. x ( ( x e. A /\ x R y ) -> y e. A ) ) |
9 |
|
19.23v |
|- ( A. x ( ( x e. A /\ x R y ) -> y e. A ) <-> ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
10 |
8 9
|
bitri |
|- ( A. x ( x e. A -> ( x R y -> y e. A ) ) <-> ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
11 |
10
|
albii |
|- ( A. y A. x ( x e. A -> ( x R y -> y e. A ) ) <-> A. y ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
12 |
4 5 11
|
3bitri |
|- ( A. x ( x e. A -> A. y ( x R y -> y e. A ) ) <-> A. y ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
13 |
|
dfss2 |
|- ( { z | E. x ( x e. A /\ <. x , z >. e. R ) } C_ A <-> A. y ( y e. { z | E. x ( x e. A /\ <. x , z >. e. R ) } -> y e. A ) ) |
14 |
|
vex |
|- y e. _V |
15 |
|
opeq2 |
|- ( z = y -> <. x , z >. = <. x , y >. ) |
16 |
15
|
eleq1d |
|- ( z = y -> ( <. x , z >. e. R <-> <. x , y >. e. R ) ) |
17 |
|
df-br |
|- ( x R y <-> <. x , y >. e. R ) |
18 |
16 17
|
bitr4di |
|- ( z = y -> ( <. x , z >. e. R <-> x R y ) ) |
19 |
18
|
anbi2d |
|- ( z = y -> ( ( x e. A /\ <. x , z >. e. R ) <-> ( x e. A /\ x R y ) ) ) |
20 |
19
|
exbidv |
|- ( z = y -> ( E. x ( x e. A /\ <. x , z >. e. R ) <-> E. x ( x e. A /\ x R y ) ) ) |
21 |
14 20
|
elab |
|- ( y e. { z | E. x ( x e. A /\ <. x , z >. e. R ) } <-> E. x ( x e. A /\ x R y ) ) |
22 |
21
|
imbi1i |
|- ( ( y e. { z | E. x ( x e. A /\ <. x , z >. e. R ) } -> y e. A ) <-> ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
23 |
22
|
albii |
|- ( A. y ( y e. { z | E. x ( x e. A /\ <. x , z >. e. R ) } -> y e. A ) <-> A. y ( E. x ( x e. A /\ x R y ) -> y e. A ) ) |
24 |
13 23
|
bitr2i |
|- ( A. y ( E. x ( x e. A /\ x R y ) -> y e. A ) <-> { z | E. x ( x e. A /\ <. x , z >. e. R ) } C_ A ) |
25 |
|
dfima3 |
|- ( R " A ) = { z | E. x ( x e. A /\ <. x , z >. e. R ) } |
26 |
25
|
eqcomi |
|- { z | E. x ( x e. A /\ <. x , z >. e. R ) } = ( R " A ) |
27 |
26
|
sseq1i |
|- ( { z | E. x ( x e. A /\ <. x , z >. e. R ) } C_ A <-> ( R " A ) C_ A ) |
28 |
24 27
|
bitri |
|- ( A. y ( E. x ( x e. A /\ x R y ) -> y e. A ) <-> ( R " A ) C_ A ) |
29 |
12 28
|
bitr2i |
|- ( ( R " A ) C_ A <-> A. x ( x e. A -> A. y ( x R y -> y e. A ) ) ) |
30 |
1 29
|
bitri |
|- ( R hereditary A <-> A. x ( x e. A -> A. y ( x R y -> y e. A ) ) ) |