Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | bnj1444.1 | |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
|
| bnj1444.2 | |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
||
| bnj1444.3 | |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
||
| bnj1444.4 | |- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
||
| bnj1444.5 | |- D = { x e. A | -. E. f ta } |
||
| bnj1444.6 | |- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
||
| bnj1444.7 | |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
||
| bnj1444.8 | |- ( ta' <-> [. y / x ]. ta ) |
||
| bnj1444.9 | |- H = { f | E. y e. _pred ( x , A , R ) ta' } |
||
| bnj1444.10 | |- P = U. H |
||
| bnj1444.11 | |- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
||
| bnj1444.12 | |- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
||
| bnj1444.13 | |- W = <. z , ( Q |` _pred ( z , A , R ) ) >. |
||
| bnj1444.14 | |- E = ( { x } u. _trCl ( x , A , R ) ) |
||
| bnj1444.15 | |- ( ch -> P Fn _trCl ( x , A , R ) ) |
||
| bnj1444.16 | |- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) ) |
||
| bnj1444.17 | |- ( th <-> ( ch /\ z e. E ) ) |
||
| bnj1444.18 | |- ( et <-> ( th /\ z e. { x } ) ) |
||
| bnj1444.19 | |- ( ze <-> ( th /\ z e. _trCl ( x , A , R ) ) ) |
||
| bnj1444.20 | |- ( rh <-> ( ze /\ f e. H /\ z e. dom f ) ) |
||
| Assertion | bnj1444 | |- ( rh -> A. y rh ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bnj1444.1 | |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
|
| 2 | bnj1444.2 | |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
|
| 3 | bnj1444.3 | |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
|
| 4 | bnj1444.4 | |- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
|
| 5 | bnj1444.5 | |- D = { x e. A | -. E. f ta } |
|
| 6 | bnj1444.6 | |- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
|
| 7 | bnj1444.7 | |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
|
| 8 | bnj1444.8 | |- ( ta' <-> [. y / x ]. ta ) |
|
| 9 | bnj1444.9 | |- H = { f | E. y e. _pred ( x , A , R ) ta' } |
|
| 10 | bnj1444.10 | |- P = U. H |
|
| 11 | bnj1444.11 | |- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
|
| 12 | bnj1444.12 | |- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
|
| 13 | bnj1444.13 | |- W = <. z , ( Q |` _pred ( z , A , R ) ) >. |
|
| 14 | bnj1444.14 | |- E = ( { x } u. _trCl ( x , A , R ) ) |
|
| 15 | bnj1444.15 | |- ( ch -> P Fn _trCl ( x , A , R ) ) |
|
| 16 | bnj1444.16 | |- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) ) |
|
| 17 | bnj1444.17 | |- ( th <-> ( ch /\ z e. E ) ) |
|
| 18 | bnj1444.18 | |- ( et <-> ( th /\ z e. { x } ) ) |
|
| 19 | bnj1444.19 | |- ( ze <-> ( th /\ z e. _trCl ( x , A , R ) ) ) |
|
| 20 | bnj1444.20 | |- ( rh <-> ( ze /\ f e. H /\ z e. dom f ) ) |
|
| 21 | nfv | |- F/ y ps |
|
| 22 | nfv | |- F/ y x e. D |
|
| 23 | nfra1 | |- F/ y A. y e. D -. y R x |
|
| 24 | 21 22 23 | nf3an | |- F/ y ( ps /\ x e. D /\ A. y e. D -. y R x ) |
| 25 | 7 24 | nfxfr | |- F/ y ch |
| 26 | nfv | |- F/ y z e. E |
|
| 27 | 25 26 | nfan | |- F/ y ( ch /\ z e. E ) |
| 28 | 17 27 | nfxfr | |- F/ y th |
| 29 | nfv | |- F/ y z e. _trCl ( x , A , R ) |
|
| 30 | 28 29 | nfan | |- F/ y ( th /\ z e. _trCl ( x , A , R ) ) |
| 31 | 19 30 | nfxfr | |- F/ y ze |
| 32 | nfre1 | |- F/ y E. y e. _pred ( x , A , R ) ta' |
|
| 33 | 32 | nfab | |- F/_ y { f | E. y e. _pred ( x , A , R ) ta' } |
| 34 | 9 33 | nfcxfr | |- F/_ y H |
| 35 | 34 | nfcri | |- F/ y f e. H |
| 36 | nfv | |- F/ y z e. dom f |
|
| 37 | 31 35 36 | nf3an | |- F/ y ( ze /\ f e. H /\ z e. dom f ) |
| 38 | 20 37 | nfxfr | |- F/ y rh |
| 39 | 38 | nf5ri | |- ( rh -> A. y rh ) |