Metamath Proof Explorer

Theorem bnj1279

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

Proof

Step Hyp Ref Expression
1 bnj1279.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1279.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1279.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1279.4 
 |-  D = ( dom g i^i dom h )
5 bnj1279.5 
 |-  E = { x e. D | ( g ` x ) =/= ( h ` x ) }
6 bnj1279.6 
 |-  ( ph <-> ( R _FrSe A /\ g e. C /\ h e. C /\ ( g |` D ) =/= ( h |` D ) ) )
7 bnj1279.7 
 |-  ( ps <-> ( ph /\ x e. E /\ A. y e. E -. y R x ) )
8 n0 
 |-  ( ( _pred ( x , A , R ) i^i E ) =/= (/) <-> E. y y e. ( _pred ( x , A , R ) i^i E ) )
9 elin 
 |-  ( y e. ( _pred ( x , A , R ) i^i E ) <-> ( y e. _pred ( x , A , R ) /\ y e. E ) )
10 9 exbii 
 |-  ( E. y y e. ( _pred ( x , A , R ) i^i E ) <-> E. y ( y e. _pred ( x , A , R ) /\ y e. E ) )
11 8 10 sylbb 
 |-  ( ( _pred ( x , A , R ) i^i E ) =/= (/) -> E. y ( y e. _pred ( x , A , R ) /\ y e. E ) )
12 df-bnj14 
 |-  _pred ( x , A , R ) = { y e. A | y R x }
13 12 bnj1538 
 |-  ( y e. _pred ( x , A , R ) -> y R x )
14 13 anim1i 
 |-  ( ( y e. _pred ( x , A , R ) /\ y e. E ) -> ( y R x /\ y e. E ) )
15 11 14 bnj593 
 |-  ( ( _pred ( x , A , R ) i^i E ) =/= (/) -> E. y ( y R x /\ y e. E ) )
16 15 3ad2ant3 
 |-  ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) -> E. y ( y R x /\ y e. E ) )
17 nfv 
 |-  F/ y x e. E
18 nfra1 
 |-  F/ y A. y e. E -. y R x
19 nfv 
 |-  F/ y ( _pred ( x , A , R ) i^i E ) =/= (/)
20 17 18 19 nf3an 
 |-  F/ y ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) )
21 20 nf5ri 
 |-  ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) -> A. y ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) )
22 16 21 bnj1275 
 |-  ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) -> E. y ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) /\ y R x /\ y e. E ) )
23 simp2 
 |-  ( ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) /\ y R x /\ y e. E ) -> y R x )
24 simp12 
 |-  ( ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) /\ y R x /\ y e. E ) -> A. y e. E -. y R x )
25 simp3 
 |-  ( ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) /\ y R x /\ y e. E ) -> y e. E )
26 24 25 bnj1294 
 |-  ( ( ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) ) /\ y R x /\ y e. E ) -> -. y R x )
27 22 23 26 bnj1304 
 |-  -. ( x e. E /\ A. y e. E -. y R x /\ ( _pred ( x , A , R ) i^i E ) =/= (/) )
28 27 bnj1224 
 |-  ( ( x e. E /\ A. y e. E -. y R x ) -> -. ( _pred ( x , A , R ) i^i E ) =/= (/) )
29 nne 
 |-  ( -. ( _pred ( x , A , R ) i^i E ) =/= (/) <-> ( _pred ( x , A , R ) i^i E ) = (/) )
30 28 29 sylib 
 |-  ( ( x e. E /\ A. y e. E -. y R x ) -> ( _pred ( x , A , R ) i^i E ) = (/) )