Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1421.1 |
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
2 |
|
bnj1421.2 |
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
3 |
|
bnj1421.3 |
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
4 |
|
bnj1421.4 |
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
5 |
|
bnj1421.5 |
|- D = { x e. A | -. E. f ta } |
6 |
|
bnj1421.6 |
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
7 |
|
bnj1421.7 |
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
8 |
|
bnj1421.8 |
|- ( ta' <-> [. y / x ]. ta ) |
9 |
|
bnj1421.9 |
|- H = { f | E. y e. _pred ( x , A , R ) ta' } |
10 |
|
bnj1421.10 |
|- P = U. H |
11 |
|
bnj1421.11 |
|- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
12 |
|
bnj1421.12 |
|- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
13 |
|
bnj1421.13 |
|- ( ch -> Fun P ) |
14 |
|
bnj1421.14 |
|- ( ch -> dom Q = ( { x } u. _trCl ( x , A , R ) ) ) |
15 |
|
bnj1421.15 |
|- ( ch -> dom P = _trCl ( x , A , R ) ) |
16 |
|
vex |
|- x e. _V |
17 |
|
fvex |
|- ( G ` Z ) e. _V |
18 |
16 17
|
funsn |
|- Fun { <. x , ( G ` Z ) >. } |
19 |
13 18
|
jctir |
|- ( ch -> ( Fun P /\ Fun { <. x , ( G ` Z ) >. } ) ) |
20 |
17
|
dmsnop |
|- dom { <. x , ( G ` Z ) >. } = { x } |
21 |
20
|
a1i |
|- ( ch -> dom { <. x , ( G ` Z ) >. } = { x } ) |
22 |
15 21
|
ineq12d |
|- ( ch -> ( dom P i^i dom { <. x , ( G ` Z ) >. } ) = ( _trCl ( x , A , R ) i^i { x } ) ) |
23 |
6
|
simplbi |
|- ( ps -> R _FrSe A ) |
24 |
7 23
|
bnj835 |
|- ( ch -> R _FrSe A ) |
25 |
|
biid |
|- ( R _FrSe A <-> R _FrSe A ) |
26 |
|
biid |
|- ( -. x e. _trCl ( x , A , R ) <-> -. x e. _trCl ( x , A , R ) ) |
27 |
|
biid |
|- ( A. z e. A ( z R x -> [. z / x ]. -. x e. _trCl ( x , A , R ) ) <-> A. z e. A ( z R x -> [. z / x ]. -. x e. _trCl ( x , A , R ) ) ) |
28 |
|
biid |
|- ( ( R _FrSe A /\ x e. A /\ A. z e. A ( z R x -> [. z / x ]. -. x e. _trCl ( x , A , R ) ) ) <-> ( R _FrSe A /\ x e. A /\ A. z e. A ( z R x -> [. z / x ]. -. x e. _trCl ( x , A , R ) ) ) ) |
29 |
|
eqid |
|- ( _pred ( x , A , R ) u. U_ z e. _pred ( x , A , R ) _trCl ( z , A , R ) ) = ( _pred ( x , A , R ) u. U_ z e. _pred ( x , A , R ) _trCl ( z , A , R ) ) |
30 |
25 26 27 28 29
|
bnj1417 |
|- ( R _FrSe A -> A. x e. A -. x e. _trCl ( x , A , R ) ) |
31 |
|
disjsn |
|- ( ( _trCl ( x , A , R ) i^i { x } ) = (/) <-> -. x e. _trCl ( x , A , R ) ) |
32 |
31
|
ralbii |
|- ( A. x e. A ( _trCl ( x , A , R ) i^i { x } ) = (/) <-> A. x e. A -. x e. _trCl ( x , A , R ) ) |
33 |
30 32
|
sylibr |
|- ( R _FrSe A -> A. x e. A ( _trCl ( x , A , R ) i^i { x } ) = (/) ) |
34 |
24 33
|
syl |
|- ( ch -> A. x e. A ( _trCl ( x , A , R ) i^i { x } ) = (/) ) |
35 |
5 7
|
bnj1212 |
|- ( ch -> x e. A ) |
36 |
34 35
|
bnj1294 |
|- ( ch -> ( _trCl ( x , A , R ) i^i { x } ) = (/) ) |
37 |
22 36
|
eqtrd |
|- ( ch -> ( dom P i^i dom { <. x , ( G ` Z ) >. } ) = (/) ) |
38 |
|
funun |
|- ( ( ( Fun P /\ Fun { <. x , ( G ` Z ) >. } ) /\ ( dom P i^i dom { <. x , ( G ` Z ) >. } ) = (/) ) -> Fun ( P u. { <. x , ( G ` Z ) >. } ) ) |
39 |
19 37 38
|
syl2anc |
|- ( ch -> Fun ( P u. { <. x , ( G ` Z ) >. } ) ) |
40 |
12
|
funeqi |
|- ( Fun Q <-> Fun ( P u. { <. x , ( G ` Z ) >. } ) ) |
41 |
39 40
|
sylibr |
|- ( ch -> Fun Q ) |