Theorem bnj1374

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	bnj1374.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj1374.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj1374.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj1374.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
	bnj1374.5	|- D = { x e. A | -. E. f ta }
	bnj1374.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
	bnj1374.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
	bnj1374.8	|- ( ta' <-> [. y / x ]. ta )
	bnj1374.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
Assertion	bnj1374	|- ( f e. H -> f e. C )

Proof

Step	Hyp	Ref	Expression
1		bnj1374.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj1374.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj1374.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj1374.4	|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5		bnj1374.5	|- D = { x e. A | -. E. f ta }
6		bnj1374.6	|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7		bnj1374.7	|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8		bnj1374.8	|- ( ta' <-> [. y / x ]. ta )
9		bnj1374.9	|- H = { f | E. y e. _pred ( x , A , R ) ta' }
10	9	bnj1436	|- ( f e. H -> E. y e. _pred ( x , A , R ) ta' )
11		rexex	|- ( E. y e. _pred ( x , A , R ) ta' -> E. y ta' )
12	10 11	syl	|- ( f e. H -> E. y ta' )
13	1 2 3 4 8	bnj1373	|- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
14	13	exbii	|- ( E. y ta' <-> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
15	12 14	sylib	|- ( f e. H -> E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
16		exsimpl	|- ( E. y ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) -> E. y f e. C )
17	15 16	syl	|- ( f e. H -> E. y f e. C )
18	17	bnj937	|- ( f e. H -> f e. C )