Metamath Proof Explorer

Theorem bnj1311

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

Proof

Step Hyp Ref Expression
1 bnj1311.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1311.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1311.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1311.4 
 |-  D = ( dom g i^i dom h )
5 biid 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
6 5 bnj1232 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> R _FrSe A )
7 ssrab2 
 |-  { x e. D | ( g ` x ) =/= ( h ` x ) } C_ D
8 5 bnj1235 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> g e. C )
9 eqid 
 |-  <. x , ( g |` _pred ( x , A , R ) ) >. = <. x , ( g |` _pred ( x , A , R ) ) >.
10 eqid 
 |-  { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) }
11 2 3 9 10 bnj1234 
 |-  C = { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) }
12 8 11 eleqtrdi 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } )
13 abid 
 |-  ( g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } <-> E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) )
14 13 bnj1238 
 |-  ( g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } -> E. d e. B g Fn d )
15 14 bnj1196 
 |-  ( g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } -> E. d ( d e. B /\ g 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 
 |-  ( g Fn d -> dom g = d )
19 17 18 bnj1241 
 |-  ( ( d e. B /\ g Fn d ) -> dom g C_ A )
20 15 19 bnj593 
 |-  ( g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } -> E. d dom g C_ A )
21 20 bnj937 
 |-  ( g e. { g | E. d e. B ( g Fn d /\ A. x e. d ( g ` x ) = ( G ` <. x , ( g |` _pred ( x , A , R ) ) >. ) ) } -> dom g C_ A )
22 ssinss1 
 |-  ( dom g C_ A -> ( dom g i^i dom h ) C_ A )
23 12 21 22 3syl 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> ( dom g i^i dom h ) C_ A )
24 4 23 eqsstrid 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> D C_ A )
25 7 24 sstrid 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> { x e. D | ( g ` x ) =/= ( h ` x ) } C_ A )
26 eqid 
 |-  { x e. D | ( g ` x ) =/= ( h ` x ) } = { x e. D | ( g ` x ) =/= ( h ` x ) }
27 biid 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) <-> ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) )
28 1 2 3 4 26 5 27 bnj1253 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> { x e. D | ( g ` x ) =/= ( h ` x ) } =/= (/) )
29 nfrab1 
 |-  F/_ x { x e. D | ( g ` x ) =/= ( h ` x ) }
30 29 nfcrii 
 |-  ( z e. { x e. D | ( g ` x ) =/= ( h ` x ) } -> A. x z e. { x e. D | ( g ` x ) =/= ( h ` x ) } )
31 30 bnj1228 
 |-  ( ( R _FrSe A /\ { x e. D | ( g ` x ) =/= ( h ` x ) } C_ A /\ { x e. D | ( g ` x ) =/= ( h ` x ) } =/= (/) ) -> E. x e. { x e. D | ( g ` x ) =/= ( h ` x ) } A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x )
32 6 25 28 31 syl3anc 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> E. x e. { x e. D | ( g ` x ) =/= ( h ` x ) } A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x )
33 ax-5 
 |-  ( R _FrSe A -> A. x R _FrSe A )
34 1 bnj1309 
 |-  ( w e. B -> A. x w e. B )
35 3 34 bnj1307 
 |-  ( w e. C -> A. x w e. C )
36 35 hblem 
 |-  ( g e. C -> A. x g e. C )
37 35 hblem 
 |-  ( h e. C -> A. x h e. C )
38 ax-5 
 |-  ( ( g |` D ) =/= ( h |` D ) -> A. x ( g |` D ) =/= ( h |` D ) )
39 33 36 37 38 bnj982 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> A. x ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
40 32 27 39 bnj1521 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) -> E. x ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) )
41 simp2 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> x e. { x e. D | ( g ` x ) =/= ( h ` x ) } )
42 1 2 3 4 26 5 27 bnj1279 
 |-  ( ( x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> ( _pred ( x , A , R ) i^i { x e. D | ( g ` x ) =/= ( h ` x ) } ) = (/) )
43 42 3adant1 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> ( _pred ( x , A , R ) i^i { x e. D | ( g ` x ) =/= ( h ` x ) } ) = (/) )
44 1 2 3 4 26 5 27 43 bnj1280 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> ( g |` _pred ( x , A , R ) ) = ( h |` _pred ( x , A , R ) ) )
45 eqid 
 |-  <. x , ( h |` _pred ( x , A , R ) ) >. = <. x , ( h |` _pred ( x , A , R ) ) >.
46 eqid 
 |-  { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) } = { h | E. d e. B ( h Fn d /\ A. x e. d ( h ` x ) = ( G ` <. x , ( h |` _pred ( x , A , R ) ) >. ) ) }
47 1 2 3 4 26 5 27 44 9 10 45 46 bnj1296 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> ( g ` x ) = ( h ` x ) )
48 26 bnj1538 
 |-  ( x e. { x e. D | ( g ` x ) =/= ( h ` x ) } -> ( g ` x ) =/= ( h ` x ) )
49 48 necon2bi 
 |-  ( ( g ` x ) = ( h ` x ) -> -. x e. { x e. D | ( g ` x ) =/= ( h ` x ) } )
50 47 49 syl 
 |-  ( ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) /\ x e. { x e. D | ( g ` x ) =/= ( h ` x ) } /\ A. y e. { x e. D | ( g ` x ) =/= ( h ` x ) } -. y R x ) -> -. x e. { x e. D | ( g ` x ) =/= ( h ` x ) } )
51 40 41 50 bnj1304 
 |-  -. ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) )
52 df-bnj17 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) <-> ( ( R _FrSe A /\ g e. C /\ h e. C ) /\ ( g |` D ) =/= ( h |` D ) ) )
53 51 52 mtbi 
 |-  -. ( ( R _FrSe A /\ g e. C /\ h e. C ) /\ ( g |` D ) =/= ( h |` D ) )
54 53 imnani 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C ) -> -. ( g |` D ) =/= ( h |` D ) )
55 nne 
 |-  ( -. ( g |` D ) =/= ( h |` D ) <-> ( g |` D ) = ( h |` D ) )
56 54 55 sylib 
 |-  ( ( R _FrSe A /\ g e. C /\ h e. C ) -> ( g |` D ) = ( h |` D ) )