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 | bnj1449.1 | |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
|
| bnj1449.2 | |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
||
| bnj1449.3 | |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
||
| bnj1449.4 | |- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
||
| bnj1449.5 | |- D = { x e. A | -. E. f ta } |
||
| bnj1449.6 | |- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
||
| bnj1449.7 | |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
||
| bnj1449.8 | |- ( ta' <-> [. y / x ]. ta ) |
||
| bnj1449.9 | |- H = { f | E. y e. _pred ( x , A , R ) ta' } |
||
| bnj1449.10 | |- P = U. H |
||
| bnj1449.11 | |- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
||
| bnj1449.12 | |- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
||
| bnj1449.13 | |- W = <. z , ( Q |` _pred ( z , A , R ) ) >. |
||
| bnj1449.14 | |- E = ( { x } u. _trCl ( x , A , R ) ) |
||
| bnj1449.15 | |- ( ch -> P Fn _trCl ( x , A , R ) ) |
||
| bnj1449.16 | |- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) ) |
||
| bnj1449.17 | |- ( th <-> ( ch /\ z e. E ) ) |
||
| bnj1449.18 | |- ( et <-> ( th /\ z e. { x } ) ) |
||
| bnj1449.19 | |- ( ze <-> ( th /\ z e. _trCl ( x , A , R ) ) ) |
||
| Assertion | bnj1449 | |- ( ze -> A. f ze ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bnj1449.1 | |- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) } |
|
| 2 | bnj1449.2 | |- Y = <. x , ( f |` _pred ( x , A , R ) ) >. |
|
| 3 | bnj1449.3 | |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) } |
|
| 4 | bnj1449.4 | |- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) |
|
| 5 | bnj1449.5 | |- D = { x e. A | -. E. f ta } |
|
| 6 | bnj1449.6 | |- ( ps <-> ( R _FrSe A /\ D =/= (/) ) ) |
|
| 7 | bnj1449.7 | |- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) ) |
|
| 8 | bnj1449.8 | |- ( ta' <-> [. y / x ]. ta ) |
|
| 9 | bnj1449.9 | |- H = { f | E. y e. _pred ( x , A , R ) ta' } |
|
| 10 | bnj1449.10 | |- P = U. H |
|
| 11 | bnj1449.11 | |- Z = <. x , ( P |` _pred ( x , A , R ) ) >. |
|
| 12 | bnj1449.12 | |- Q = ( P u. { <. x , ( G ` Z ) >. } ) |
|
| 13 | bnj1449.13 | |- W = <. z , ( Q |` _pred ( z , A , R ) ) >. |
|
| 14 | bnj1449.14 | |- E = ( { x } u. _trCl ( x , A , R ) ) |
|
| 15 | bnj1449.15 | |- ( ch -> P Fn _trCl ( x , A , R ) ) |
|
| 16 | bnj1449.16 | |- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) ) |
|
| 17 | bnj1449.17 | |- ( th <-> ( ch /\ z e. E ) ) |
|
| 18 | bnj1449.18 | |- ( et <-> ( th /\ z e. { x } ) ) |
|
| 19 | bnj1449.19 | |- ( ze <-> ( th /\ z e. _trCl ( x , A , R ) ) ) |
|
| 20 | nfv | |- F/ f R _FrSe A |
|
| 21 | nfe1 | |- F/ f E. f ta |
|
| 22 | 21 | nfn | |- F/ f -. E. f ta |
| 23 | nfcv | |- F/_ f A |
|
| 24 | 22 23 | nfrabw | |- F/_ f { x e. A | -. E. f ta } |
| 25 | 5 24 | nfcxfr | |- F/_ f D |
| 26 | nfcv | |- F/_ f (/) |
|
| 27 | 25 26 | nfne | |- F/ f D =/= (/) |
| 28 | 20 27 | nfan | |- F/ f ( R _FrSe A /\ D =/= (/) ) |
| 29 | 6 28 | nfxfr | |- F/ f ps |
| 30 | 25 | nfcri | |- F/ f x e. D |
| 31 | nfv | |- F/ f -. y R x |
|
| 32 | 25 31 | nfralw | |- F/ f A. y e. D -. y R x |
| 33 | 29 30 32 | nf3an | |- F/ f ( ps /\ x e. D /\ A. y e. D -. y R x ) |
| 34 | 7 33 | nfxfr | |- F/ f ch |
| 35 | nfv | |- F/ f z e. E |
|
| 36 | 34 35 | nfan | |- F/ f ( ch /\ z e. E ) |
| 37 | 17 36 | nfxfr | |- F/ f th |
| 38 | nfv | |- F/ f z e. _trCl ( x , A , R ) |
|
| 39 | 37 38 | nfan | |- F/ f ( th /\ z e. _trCl ( x , A , R ) ) |
| 40 | 19 39 | nfxfr | |- F/ f ze |
| 41 | 40 | nf5ri | |- ( ze -> A. f ze ) |