Metamath Proof Explorer

Theorem bnj1245

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 bnj1245.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1245.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1245.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1245.4 
|- D = ( dom g i^i dom h )
bnj1245.5 
|- E = { x e. D | ( g ` x ) =/= ( h ` x ) }
bnj1245.6 
|- ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
bnj1245.7 
|- ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
bnj1245.8 
|- Z = <. x , ( h |` _pred ( x , A , R ) ) >.
bnj1245.9 
|- K = { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` Z ) ) }
Assertion bnj1245 
|- ( ph -> dom h C_ A )

Proof

Step Hyp Ref Expression
1 bnj1245.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1245.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1245.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1245.4 
 |-  D = ( dom g i^i dom h )
5 bnj1245.5 
 |-  E = { x e. D | ( g ` x ) =/= ( h ` x ) }
6 bnj1245.6 
 |-  ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
7 bnj1245.7 
 |-  ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8 bnj1245.8 
 |-  Z = <. x , ( h |` _pred ( x , A , R ) ) >.
9 bnj1245.9 
 |-  K = { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` Z ) ) }
10 6 bnj1247 
 |-  ( ph -> h e. C )
11 2 3 8 9 bnj1234 
 |-  C = K
12 10 11 eleqtrdi 
 |-  ( ph -> h e. K )
13 9 abeq2i 
 |-  ( h e. K <-> E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` Z ) ) )
14 13 bnj1238 
 |-  ( h e. K -> E. d e. B h Fn d )
15 14 bnj1196 
 |-  ( h e. K -> E. d ( d e. B /\ h Fn d ) )
16 1 abeq2i 
 |-  ( d e. B <-> ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) )
17 16 simplbi 
 |-  ( d e. B -> d C_ A )
18 fndm 
 |-  ( h Fn d -> dom h = d )
19 17 18 bnj1241 
 |-  ( ( d e. B /\ h Fn d ) -> dom h C_ A )
20 15 19 bnj593 
 |-  ( h e. K -> E. d dom h C_ A )
21 20 bnj937 
 |-  ( h e. K -> dom h C_ A )
22 12 21 syl 
 |-  ( ph -> dom h C_ A )