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 )