Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1491.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1491.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1491.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1491.4 |
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
5 |
|
bnj1491.5 |
|- D = { x e. A | -. E. f ta } |
6 |
|
bnj1491.6 |
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
7 |
|
bnj1491.7 |
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
8 |
|
bnj1491.8 |
|- ( ta' <-> [. y / x ]. ta ) |
9 |
|
bnj1491.9 |
|- H = { f | E. y e. _pred ( x , A , R ) ta' } |
10 |
|
bnj1491.10 |
|- P = U. H |
11 |
|
bnj1491.11 |
|- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
12 |
|
bnj1491.12 |
|- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
13 |
|
bnj1491.13 |
|- ( ch -> ( Q e. C /\ dom Q = ( { x } u. _trCl ( x , A , R ) ) ) ) |
14 |
1 2 3 4 5 6 7 8 9 10 11 12
|
bnj1466 |
|- ( w e. Q -> A. f w e. Q ) |
15 |
14
|
nfcii |
|- F/_ f Q |
16 |
3
|
bnj1317 |
|- ( w e. C -> A. f w e. C ) |
17 |
16
|
nfcii |
|- F/_ f C |
18 |
15 17
|
nfel |
|- F/ f Q e. C |
19 |
15
|
nfdm |
|- F/_ f dom Q |
20 |
19
|
nfeq1 |
|- F/ f dom Q = ( { x } u. _trCl ( x , A , R ) ) |
21 |
18 20
|
nfan |
|- F/ f ( Q e. C /\ dom Q = ( { x } u. _trCl ( x , A , R ) ) ) |
22 |
|
eleq1 |
|- ( f = Q -> ( f e. C <-> Q e. C ) ) |
23 |
|
dmeq |
|- ( f = Q -> dom f = dom Q ) |
24 |
23
|
eqeq1d |
|- ( f = Q -> ( dom f = ( { x } u. _trCl ( x , A , R ) ) <-> dom Q = ( { x } u. _trCl ( x , A , R ) ) ) ) |
25 |
22 24
|
anbi12d |
|- ( f = Q -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ( Q e. C /\ dom Q = ( { x } u. _trCl ( x , A , R ) ) ) ) ) |
26 |
15 21 25
|
spcegf |
|- ( Q e. _V -> ( ( Q e. C /\ dom Q = ( { x } u. _trCl ( x , A , R ) ) ) -> E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) ) |
27 |
13 26
|
mpan9 |
|- ( ( ch /\ Q e. _V ) -> E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |