bnj1497

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	bnj1497.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1497.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
	bnj1497.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
Assertion	bnj1497	\|- A. g e. C Fun g

Proof

Step	Hyp	Ref	Expression
1		bnj1497.1	\|- B = { d \| ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1497.2	\|- Y = <. x , ( f \|` _pred ( x , A , R ) ) >.
3		bnj1497.3	\|- C = { f \| E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4	3	bnj1317	\|- ( g e. C -> A. f g e. C )
5	4	nf5i	\|- F/ f g e. C
6		nfv	\|- F/ f Fun g
7	5 6	nfim	\|- F/ f ( g e. C -> Fun g )
8		eleq1w	\|- ( f = g -> ( f e. C <-> g e. C ) )
9		funeq	\|- ( f = g -> ( Fun f <-> Fun g ) )
10	8 9	imbi12d	\|- ( f = g -> ( ( f e. C -> Fun f ) <-> ( g e. C -> Fun g ) ) )
11	3	bnj1436	\|- ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
12	11	bnj1299	\|- ( f e. C -> E. d e. B f Fn d )
13		fnfun	\|- ( f Fn d -> Fun f )
14	12 13	bnj31	\|- ( f e. C -> E. d e. B Fun f )
15	14	bnj1265	\|- ( f e. C -> Fun f )
16	7 10 15	chvarfv	\|- ( g e. C -> Fun g )
17	16	rgen	\|- A. g e. C Fun g

Metamath Proof Explorer

Theorem bnj1497

Proof