Metamath Proof Explorer


Theorem bnj1259

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 bnj1259.1
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1259.2
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1259.3
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1259.4
|- D = ( dom g i^i dom h )
bnj1259.5
|- E = { x e. D | ( g ` x ) =/= ( h ` x ) }
bnj1259.6
|- ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
bnj1259.7
|- ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
Assertion bnj1259
|- ( ph -> E. d e. B h Fn d )

Proof

Step Hyp Ref Expression
1 bnj1259.1
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1259.2
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1259.3
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1259.4
 |-  D = ( dom g i^i dom h )
5 bnj1259.5
 |-  E = { x e. D | ( g ` x ) =/= ( h ` x ) }
6 bnj1259.6
 |-  ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
7 bnj1259.7
 |-  ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8 abid
 |-  ( h e. { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) } <-> E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) )
9 8 bnj1238
 |-  ( h e. { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) } -> E. d e. B h Fn d )
10 eqid
 |-  <. x , ( h |` _pred ( x , A , R ) ) >. = <. x , ( h |` _pred ( x , A , R ) ) >.
11 eqid
 |-  { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) } = { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) }
12 2 3 10 11 bnj1234
 |-  C = { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) }
13 9 12 eleq2s
 |-  ( h e. C -> E. d e. B h Fn d )
14 6 13 bnj771
 |-  ( ph -> E. d e. B h Fn d )