Theorem bnj1256

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

Proof

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