Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1498.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1498.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1498.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1498.4 |
|- F = U. C |
5 |
|
eliun |
|- ( z e. U_ f e. C dom f <-> E. f e. C z e. dom f ) |
6 |
3
|
bnj1436 |
|- ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) |
7 |
6
|
bnj1299 |
|- ( f e. C -> E. d e. B f Fn d ) |
8 |
|
fndm |
|- ( f Fn d -> dom f = d ) |
9 |
7 8
|
bnj31 |
|- ( f e. C -> E. d e. B dom f = d ) |
10 |
9
|
bnj1196 |
|- ( f e. C -> E. d ( d e. B /\ dom f = d ) ) |
11 |
1
|
bnj1436 |
|- ( d e. B -> ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) ) |
12 |
11
|
simpld |
|- ( d e. B -> d C_ A ) |
13 |
12
|
anim1i |
|- ( ( d e. B /\ dom f = d ) -> ( d C_ A /\ dom f = d ) ) |
14 |
10 13
|
bnj593 |
|- ( f e. C -> E. d ( d C_ A /\ dom f = d ) ) |
15 |
|
sseq1 |
|- ( dom f = d -> ( dom f C_ A <-> d C_ A ) ) |
16 |
15
|
biimparc |
|- ( ( d C_ A /\ dom f = d ) -> dom f C_ A ) |
17 |
14 16
|
bnj593 |
|- ( f e. C -> E. d dom f C_ A ) |
18 |
17
|
bnj937 |
|- ( f e. C -> dom f C_ A ) |
19 |
18
|
sselda |
|- ( ( f e. C /\ z e. dom f ) -> z e. A ) |
20 |
19
|
rexlimiva |
|- ( E. f e. C z e. dom f -> z e. A ) |
21 |
5 20
|
sylbi |
|- ( z e. U_ f e. C dom f -> z e. A ) |
22 |
3
|
bnj1317 |
|- ( w e. C -> A. f w e. C ) |
23 |
22
|
bnj1400 |
|- dom U. C = U_ f e. C dom f |
24 |
21 23
|
eleq2s |
|- ( z e. dom U. C -> z e. A ) |
25 |
4
|
dmeqi |
|- dom F = dom U. C |
26 |
24 25
|
eleq2s |
|- ( z e. dom F -> z e. A ) |
27 |
26
|
ssriv |
|- dom F C_ A |
28 |
27
|
a1i |
|- ( R _FrSe A -> dom F C_ A ) |
29 |
1 2 3
|
bnj1493 |
|- ( R _FrSe A -> A. x e. A E. f e. C dom f = ( { x } u. _trCl ( x , A , R ) ) ) |
30 |
|
vsnid |
|- x e. { x } |
31 |
|
elun1 |
|- ( x e. { x } -> x e. ( { x } u. _trCl ( x , A , R ) ) ) |
32 |
30 31
|
ax-mp |
|- x e. ( { x } u. _trCl ( x , A , R ) ) |
33 |
|
eleq2 |
|- ( dom f = ( { x } u. _trCl ( x , A , R ) ) -> ( x e. dom f <-> x e. ( { x } u. _trCl ( x , A , R ) ) ) ) |
34 |
32 33
|
mpbiri |
|- ( dom f = ( { x } u. _trCl ( x , A , R ) ) -> x e. dom f ) |
35 |
34
|
reximi |
|- ( E. f e. C dom f = ( { x } u. _trCl ( x , A , R ) ) -> E. f e. C x e. dom f ) |
36 |
35
|
ralimi |
|- ( A. x e. A E. f e. C dom f = ( { x } u. _trCl ( x , A , R ) ) -> A. x e. A E. f e. C x e. dom f ) |
37 |
29 36
|
syl |
|- ( R _FrSe A -> A. x e. A E. f e. C x e. dom f ) |
38 |
|
eliun |
|- ( x e. U_ f e. C dom f <-> E. f e. C x e. dom f ) |
39 |
38
|
ralbii |
|- ( A. x e. A x e. U_ f e. C dom f <-> A. x e. A E. f e. C x e. dom f ) |
40 |
37 39
|
sylibr |
|- ( R _FrSe A -> A. x e. A x e. U_ f e. C dom f ) |
41 |
|
nfcv |
|- F/_ x A |
42 |
1
|
bnj1309 |
|- ( t e. B -> A. x t e. B ) |
43 |
3 42
|
bnj1307 |
|- ( t e. C -> A. x t e. C ) |
44 |
43
|
nfcii |
|- F/_ x C |
45 |
|
nfcv |
|- F/_ x dom f |
46 |
44 45
|
nfiun |
|- F/_ x U_ f e. C dom f |
47 |
41 46
|
dfss3f |
|- ( A C_ U_ f e. C dom f <-> A. x e. A x e. U_ f e. C dom f ) |
48 |
40 47
|
sylibr |
|- ( R _FrSe A -> A C_ U_ f e. C dom f ) |
49 |
48 23
|
sseqtrrdi |
|- ( R _FrSe A -> A C_ dom U. C ) |
50 |
49 25
|
sseqtrrdi |
|- ( R _FrSe A -> A C_ dom F ) |
51 |
28 50
|
eqssd |
|- ( R _FrSe A -> dom F = A ) |