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 )

Metamath Proof Explorer

Theorem bnj1259

Proof