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