bnj1514

Description: Technical lemma for bnj1500 . 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	bnj1514.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1514.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
	bnj1514.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
Assertion	bnj1514	\|- ( f e. C -> A. x e. dom f ( f ` x ) = ( G ` Y ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1514.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1514.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1514.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4	3	bnj1436	\|- ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
5		df-rex	\|- ( E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> E. d ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
6		3anass	\|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
7	5 6	bnj133	\|- ( E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> E. d ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
8	4 7	sylib	\|- ( f e. C -> E. d ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
9		simp3	\|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> A. x e. d ( f ` x ) = ( G ` Y ) )
10		fndm	\|- ( f Fn d -> dom f = d )
11	10	3ad2ant2	\|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> dom f = d )
12	9 11	raleqtrrdv	\|- ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) -> A. x e. dom f ( f ` x ) = ( G ` Y ) )
13	8 12	bnj593	\|- ( f e. C -> E. d A. x e. dom f ( f ` x ) = ( G ` Y ) )
14	13	bnj937	\|- ( f e. C -> A. x e. dom f ( f ` x ) = ( G ` Y ) )

Metamath Proof Explorer

Theorem bnj1514

Proof