Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1500.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1500.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1500.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1500.4 |
|- F = U. C |
5 |
|
biid |
|- ( ( R _FrSe A /\ x e. A ) <-> ( R _FrSe A /\ x e. A ) ) |
6 |
|
biid |
|- ( ( ( R _FrSe A /\ x e. A ) /\ f e. C /\ x e. dom f ) <-> ( ( R _FrSe A /\ x e. A ) /\ f e. C /\ x e. dom f ) ) |
7 |
|
biid |
|- ( ( ( ( R _FrSe A /\ x e. A ) /\ f e. C /\ x e. dom f ) /\ d e. B /\ dom f = d ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ f e. C /\ x e. dom f ) /\ d e. B /\ dom f = d ) ) |
8 |
1 2 3 4 5 6 7
|
bnj1501 |
|- ( R _FrSe A -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) ) |