This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1280

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

Proof

Step Hyp Ref Expression
1 bnj1280.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1280.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1280.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1280.4 
 |-  D = ( dom g i^i dom h )
5 bnj1280.5 
 |-  E = { x e. D | ( g ` x ) =/= ( h ` x ) }
6 bnj1280.6 
 |-  ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
7 bnj1280.7 
 |-  ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8 bnj1280.17 
 |-  ( ps -> ( _pred ( x , A , R ) i^i E ) = (/) )
9 1 2 3 4 5 6 7 bnj1286 
 |-  ( ps -> _pred ( x , A , R ) C_ D )
10 9 sseld 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> z e. D ) )
11 disj1 
 |-  ( ( _pred ( x , A , R ) i^i E ) = (/) <-> A. z ( z e. _pred ( x , A , R ) -> -. z e. E ) )
12 8 11 sylib 
 |-  ( ps -> A. z ( z e. _pred ( x , A , R ) -> -. z e. E ) )
13 12 19.21bi 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> -. z e. E ) )
14 fveq2 
 |-  ( x = z -> ( g ` x ) = ( g ` z ) )
15 fveq2 
 |-  ( x = z -> ( h ` x ) = ( h ` z ) )
16 14 15 neeq12d 
 |-  ( x = z -> ( ( g ` x ) =/= ( h ` x ) <-> ( g ` z ) =/= ( h ` z ) ) )
17 16 5 elrab2 
 |-  ( z e. E <-> ( z e. D /\ ( g ` z ) =/= ( h ` z ) ) )
18 17 notbii 
 |-  ( -. z e. E <-> -. ( z e. D /\ ( g ` z ) =/= ( h ` z ) ) )
19 imnan 
 |-  ( ( z e. D -> -. ( g ` z ) =/= ( h ` z ) ) <-> -. ( z e. D /\ ( g ` z ) =/= ( h ` z ) ) )
20 nne 
 |-  ( -. ( g ` z ) =/= ( h ` z ) <-> ( g ` z ) = ( h ` z ) )
21 20 imbi2i 
 |-  ( ( z e. D -> -. ( g ` z ) =/= ( h ` z ) ) <-> ( z e. D -> ( g ` z ) = ( h ` z ) ) )
22 18 19 21 3bitr2i 
 |-  ( -. z e. E <-> ( z e. D -> ( g ` z ) = ( h ` z ) ) )
23 13 22 imbitrdi 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> ( z e. D -> ( g ` z ) = ( h ` z ) ) ) )
24 10 23 mpdd 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> ( g ` z ) = ( h ` z ) ) )
25 24 imp 
 |-  ( ( ps /\ z e. _pred ( x , A , R ) ) -> ( g ` z ) = ( h ` z ) )
26 fvres 
 |-  ( z e. D -> ( ( g |` D ) ` z ) = ( g ` z ) )
27 10 26 syl6 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> ( ( g |` D ) ` z ) = ( g ` z ) ) )
28 27 imp 
 |-  ( ( ps /\ z e. _pred ( x , A , R ) ) -> ( ( g |` D ) ` z ) = ( g ` z ) )
29 fvres 
 |-  ( z e. D -> ( ( h |` D ) ` z ) = ( h ` z ) )
30 10 29 syl6 
 |-  ( ps -> ( z e. _pred ( x , A , R ) -> ( ( h |` D ) ` z ) = ( h ` z ) ) )
31 30 imp 
 |-  ( ( ps /\ z e. _pred ( x , A , R ) ) -> ( ( h |` D ) ` z ) = ( h ` z ) )
32 25 28 31 3eqtr4d 
 |-  ( ( ps /\ z e. _pred ( x , A , R ) ) -> ( ( g |` D ) ` z ) = ( ( h |` D ) ` z ) )
33 32 ralrimiva 
 |-  ( ps -> A. z e. _pred ( x , A , R ) ( ( g |` D ) ` z ) = ( ( h |` D ) ` z ) )
34 9 resabs1d 
 |-  ( ps -> ( ( g |` D ) |` _pred ( x , A , R ) ) = ( g |` _pred ( x , A , R ) ) )
35 9 resabs1d 
 |-  ( ps -> ( ( h |` D ) |` _pred ( x , A , R ) ) = ( h |` _pred ( x , A , R ) ) )
36 34 35 eqeq12d 
 |-  ( ps -> ( ( ( g |` D ) |` _pred ( x , A , R ) ) = ( ( h |` D ) |` _pred ( x , A , R ) ) <-> ( g |` _pred ( x , A , R ) ) = ( h |` _pred ( x , A , R ) ) ) )
37 1 2 3 4 5 6 7 bnj1256 
 |-  ( ph -> E. d e. B g Fn d )
38 4 bnj1292 
 |-  D C_ dom g
39 fndm 
 |-  ( g Fn d -> dom g = d )
40 38 39 sseqtrid 
 |-  ( g Fn d -> D C_ d )
41 fnssres 
 |-  ( ( g Fn d /\ D C_ d ) -> ( g |` D ) Fn D )
42 40 41 mpdan 
 |-  ( g Fn d -> ( g |` D ) Fn D )
43 37 42 bnj31 
 |-  ( ph -> E. d e. B ( g |` D ) Fn D )
44 43 bnj1265 
 |-  ( ph -> ( g |` D ) Fn D )
45 7 44 bnj835 
 |-  ( ps -> ( g |` D ) Fn D )
46 1 2 3 4 5 6 7 bnj1259 
 |-  ( ph -> E. d e. B h Fn d )
47 4 bnj1293 
 |-  D C_ dom h
48 fndm 
 |-  ( h Fn d -> dom h = d )
49 47 48 sseqtrid 
 |-  ( h Fn d -> D C_ d )
50 fnssres 
 |-  ( ( h Fn d /\ D C_ d ) -> ( h |` D ) Fn D )
51 49 50 mpdan 
 |-  ( h Fn d -> ( h |` D ) Fn D )
52 46 51 bnj31 
 |-  ( ph -> E. d e. B ( h |` D ) Fn D )
53 52 bnj1265 
 |-  ( ph -> ( h |` D ) Fn D )
54 7 53 bnj835 
 |-  ( ps -> ( h |` D ) Fn D )
55 fvreseq 
 |-  ( ( ( ( g |` D ) Fn D /\ ( h |` D ) Fn D ) /\ _pred ( x , A , R ) C_ D ) -> ( ( ( g |` D ) |` _pred ( x , A , R ) ) = ( ( h |` D ) |` _pred ( x , A , R ) ) <-> A. z e. _pred ( x , A , R ) ( ( g |` D ) ` z ) = ( ( h |` D ) ` z ) ) )
56 45 54 9 55 syl21anc 
 |-  ( ps -> ( ( ( g |` D ) |` _pred ( x , A , R ) ) = ( ( h |` D ) |` _pred ( x , A , R ) ) <-> A. z e. _pred ( x , A , R ) ( ( g |` D ) ` z ) = ( ( h |` D ) ` z ) ) )
57 36 56 bitr3d 
 |-  ( ps -> ( ( g |` _pred ( x , A , R ) ) = ( h |` _pred ( x , A , R ) ) <-> A. z e. _pred ( x , A , R ) ( ( g |` D ) ` z ) = ( ( h |` D ) ` z ) ) )
58 33 57 mpbird 
 |-  ( ps -> ( g |` _pred ( x , A , R ) ) = ( h |` _pred ( x , A , R ) ) )