Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1514.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1514.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1514.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
3
|
bnj1436 |
|- ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) |
5 |
|
df-rex |
|- ( E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> E. d ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) ) |
6 |
|
3anass |
|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) ) |
7 |
5 6
|
bnj133 |
|- ( E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> E. d ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) |
8 |
4 7
|
sylib |
|- ( f e. C -> E. d ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) |
9 |
|
simp3 |
|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> A. x e. d ( f ` x ) = ( G ` Y ) ) |
10 |
|
fndm |
|- ( f Fn d -> dom f = d ) |
11 |
10
|
3ad2ant2 |
|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> dom f = d ) |
12 |
11
|
raleqdv |
|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> ( A. x e. dom f ( f ` x ) = ( G ` Y ) <-> A. x e. d ( f ` x ) = ( G ` Y ) ) ) |
13 |
9 12
|
mpbird |
|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> A. x e. dom f ( f ` x ) = ( G ` Y ) ) |
14 |
8 13
|
bnj593 |
|- ( f e. C -> E. d A. x e. dom f ( f ` x ) = ( G ` Y ) ) |
15 |
14
|
bnj937 |
|- ( f e. C -> A. x e. dom f ( f ` x ) = ( G ` Y ) ) |