Metamath Proof Explorer

Theorem 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 ) )