Theorem bnj1518

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

Proof

Step	Hyp	Ref	Expression
1		bnj1518.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1518.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1518.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1518.4	|- F = U. C
5		bnj1518.5	|- ( ph <-> ( R _FrSe A /\ x e. A ) )
6		bnj1518.6	|- ( ps <-> ( ph /\ f e. C /\ x e. dom f ) )
7		nfv	|- F/ d ph
8		nfre1	|- F/ d E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) )
9	8	nfab	|- F/_ d { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
10	3 9	nfcxfr	|- F/_ d C
11	10	nfcri	|- F/ d f e. C
12		nfv	|- F/ d x e. dom f
13	7 11 12	nf3an	|- F/ d ( ph /\ f e. C /\ x e. dom f )
14	6 13	nfxfr	|- F/ d ps
15	14	nf5ri	|- ( ps -> A. d ps )