Metamath Proof Explorer

Theorem bnj1253

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

Proof

Step Hyp Ref Expression
1 bnj1253.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1253.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1253.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1253.4 
 |-  D = ( dom g i^i dom h )
5 bnj1253.5 
 |-  E = { x e. D | ( g ` x ) =/= ( h ` x ) }
6 bnj1253.6 
 |-  ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
7 bnj1253.7 
 |-  ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8 6 bnj1254 
 |-  ( ph -> ( g |` D ) =/= ( h |` D ) )
9 1 2 3 4 5 6 7 bnj1256 
 |-  ( ph -> E. d e. B g Fn d )
10 4 bnj1292 
 |-  D C_ dom g
11 fndm 
 |-  ( g Fn d -> dom g = d )
12 10 11 sseqtrid 
 |-  ( g Fn d -> D C_ d )
13 fnssres 
 |-  ( ( g Fn d /\ D C_ d ) -> ( g |` D ) Fn D )
14 12 13 mpdan 
 |-  ( g Fn d -> ( g |` D ) Fn D )
15 9 14 bnj31 
 |-  ( ph -> E. d e. B ( g |` D ) Fn D )
16 15 bnj1265 
 |-  ( ph -> ( g |` D ) Fn D )
17 1 2 3 4 5 6 7 bnj1259 
 |-  ( ph -> E. d e. B h Fn d )
18 4 bnj1293 
 |-  D C_ dom h
19 fndm 
 |-  ( h Fn d -> dom h = d )
20 18 19 sseqtrid 
 |-  ( h Fn d -> D C_ d )
21 fnssres 
 |-  ( ( h Fn d /\ D C_ d ) -> ( h |` D ) Fn D )
22 20 21 mpdan 
 |-  ( h Fn d -> ( h |` D ) Fn D )
23 17 22 bnj31 
 |-  ( ph -> E. d e. B ( h |` D ) Fn D )
24 23 bnj1265 
 |-  ( ph -> ( h |` D ) Fn D )
25 ssid 
 |-  D C_ D
26 fvreseq 
 |-  ( ( ( ( g |` D ) Fn D /\ ( h |` D ) Fn D ) /\ D C_ D ) -> ( ( ( g |` D ) |` D ) = ( ( h |` D ) |` D ) <-> A. x e. D ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) )
27 25 26 mpan2 
 |-  ( ( ( g |` D ) Fn D /\ ( h |` D ) Fn D ) -> ( ( ( g |` D ) |` D ) = ( ( h |` D ) |` D ) <-> A. x e. D ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) )
28 16 24 27 syl2anc 
 |-  ( ph -> ( ( ( g |` D ) |` D ) = ( ( h |` D ) |` D ) <-> A. x e. D ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) )
29 residm 
 |-  ( ( g |` D ) |` D ) = ( g |` D )
30 residm 
 |-  ( ( h |` D ) |` D ) = ( h |` D )
31 29 30 eqeq12i 
 |-  ( ( ( g |` D ) |` D ) = ( ( h |` D ) |` D ) <-> ( g |` D ) = ( h |` D ) )
32 df-ral 
 |-  ( A. x e. D ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) <-> A. x ( x e. D -> ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) )
33 28 31 32 3bitr3g 
 |-  ( ph -> ( ( g |` D ) = ( h |` D ) <-> A. x ( x e. D -> ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) ) )
34 fvres 
 |-  ( x e. D -> ( ( g |` D ) ` x ) = ( g ` x ) )
35 fvres 
 |-  ( x e. D -> ( ( h |` D ) ` x ) = ( h ` x ) )
36 34 35 eqeq12d 
 |-  ( x e. D -> ( ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) <-> ( g ` x ) = ( h ` x ) ) )
37 36 pm5.74i 
 |-  ( ( x e. D -> ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) <-> ( x e. D -> ( g ` x ) = ( h ` x ) ) )
38 37 albii 
 |-  ( A. x ( x e. D -> ( ( g |` D ) ` x ) = ( ( h |` D ) ` x ) ) <-> A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) )
39 33 38 bitrdi 
 |-  ( ph -> ( ( g |` D ) = ( h |` D ) <-> A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) ) )
40 39 necon3abid 
 |-  ( ph -> ( ( g |` D ) =/= ( h |` D ) <-> -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) ) )
41 df-rex 
 |-  ( E. x e. D ( g ` x ) =/= ( h ` x ) <-> E. x ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
42 pm4.61 
 |-  ( -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> ( x e. D /\ -. ( g ` x ) = ( h ` x ) ) )
43 df-ne 
 |-  ( ( g ` x ) =/= ( h ` x ) <-> -. ( g ` x ) = ( h ` x ) )
44 43 anbi2i 
 |-  ( ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) <-> ( x e. D /\ -. ( g ` x ) = ( h ` x ) ) )
45 42 44 bitr4i 
 |-  ( -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
46 45 exbii 
 |-  ( E. x -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> E. x ( x e. D /\ ( g ` x ) =/= ( h ` x ) ) )
47 exnal 
 |-  ( E. x -. ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) )
48 41 46 47 3bitr2ri 
 |-  ( -. A. x ( x e. D -> ( g ` x ) = ( h ` x ) ) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
49 40 48 bitrdi 
 |-  ( ph -> ( ( g |` D ) =/= ( h |` D ) <-> E. x e. D ( g ` x ) =/= ( h ` x ) ) )
50 8 49 mpbid 
 |-  ( ph -> E. x e. D ( g ` x ) =/= ( h ` x ) )
51 5 neeq1i 
 |-  ( E =/= (/) <-> { x e. D | ( g ` x ) =/= ( h ` x ) } =/= (/) )
52 rabn0 
 |-  ( { x e. D | ( g ` x ) =/= ( h ` x ) } =/= (/) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
53 51 52 bitri 
 |-  ( E =/= (/) <-> E. x e. D ( g ` x ) =/= ( h ` x ) )
54 50 53 sylibr 
 |-  ( ph -> E =/= (/) )