Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elima4 Structured version   Visualization version   Unicode version
Theorem elima4 31679
Description: Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.)
Assertion
Ref Expression
elima4 |- ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) )
Proof of Theorem elima4
Dummy variables x p y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3212 . 2 |- ( A e. ( R " B ) -> A e. _V )
2 xpeq2 5129 . . . . . . 7 |- ( { A } = (/) -> ( B X. { A } ) = ( B X. (/) ) )
3 xp0 5552 . . . . . . 7 |- ( B X. (/) ) = (/)
42, 3syl6eq 2672 . . . . . 6 |- ( { A } = (/) -> ( B X. { A } ) = (/) )
54ineq2d 3814 . . . . 5 |- ( { A } = (/) -> ( R i^i ( B X. { A } ) ) = ( R i^i (/) ) )
6 in0 3968 . . . . 5 |- ( R i^i (/) ) = (/)
75, 6syl6eq 2672 . . . 4 |- ( { A } = (/) -> ( R i^i ( B X. { A } ) ) = (/) )
87necon3i 2826 . . 3 |- ( ( R i^i ( B X. { A } ) ) =/= (/) -> { A } =/= (/) )
9 snnzb 4254 . . 3 |- ( A e. _V <-> { A } =/= (/) )
108, 9sylibr 224 . 2 |- ( ( R i^i ( B X. { A } ) ) =/= (/) -> A e. _V )
11 eleq1 2689 . . 3 |- ( x = A -> ( x e. ( R " B ) <-> A e. ( R " B ) ) )
12 sneq 4187 . . . . . 6 |- ( x = A -> { x } = { A } )
1312xpeq2d 5139 . . . . 5 |- ( x = A -> ( B X. { x } ) = ( B X. { A } ) )
1413ineq2d 3814 . . . 4 |- ( x = A -> ( R i^i ( B X. { x } ) ) = ( R i^i ( B X. { A } ) ) )
1514neeq1d 2853 . . 3 |- ( x = A -> ( ( R i^i ( B X. { x } ) ) =/= (/) <-> ( R i^i ( B X. { A } ) ) =/= (/) ) )
16 elin 3796 . . . . . . 7 |- ( p e. ( R i^i ( B X. { x } ) ) <-> ( p e. R /\ p e. ( B X. { x } ) ) )
17 ancom 466 . . . . . . 7 |- ( ( p e. R /\ p e. ( B X. { x } ) ) <-> ( p e. ( B X. { x } ) /\ p e. R ) )
18 elxp 5131 . . . . . . . 8 |- ( p e. ( B X. { x } ) <-> E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) )
1918anbi1i 731 . . . . . . 7 |- ( ( p e. ( B X. { x } ) /\ p e. R ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
2016, 17, 193bitri 286 . . . . . 6 |- ( p e. ( R i^i ( B X. { x } ) ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
2120exbii 1774 . . . . 5 |- ( E. p p e. ( R i^i ( B X. { x } ) ) <-> E. p ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
22 anass 681 . . . . . . . . 9 |- ( ( ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) <-> ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) )
23222exbii 1775 . . . . . . . 8 |- ( E. y E. z ( ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) <-> E. y E. z ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) )
24 19.41vv 1915 . . . . . . . 8 |- ( E. y E. z ( ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
2523, 24bitr3i 266 . . . . . . 7 |- ( E. y E. z ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
2625exbii 1774 . . . . . 6 |- ( E. p E. y E. z ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> E. p ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
27 exrot3 2045 . . . . . 6 |- ( E. p E. y E. z ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> E. y E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) )
2826, 27bitr3i 266 . . . . 5 |- ( E. p ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) <-> E. y E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) )
29 opex 4932 . . . . . . . . 9 |- <. y , z >. e. _V
30 eleq1 2689 . . . . . . . . . 10 |- ( p = <. y , z >. -> ( p e. R <-> <. y , z >. e. R ) )
3130anbi2d 740 . . . . . . . . 9 |- ( p = <. y , z >. -> ( ( ( y e. B /\ z e. { x } ) /\ p e. R ) <-> ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) ) )
3229, 31ceqsexv 3242 . . . . . . . 8 |- ( E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) )
3332exbii 1774 . . . . . . 7 |- ( E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> E. z ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) )
34 anass 681 . . . . . . . . 9 |- ( ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) <-> ( y e. B /\ ( z e. { x } /\ <. y , z >. e. R ) ) )
35 an12 838 . . . . . . . . 9 |- ( ( y e. B /\ ( z e. { x } /\ <. y , z >. e. R ) ) <-> ( z e. { x } /\ ( y e. B /\ <. y , z >. e. R ) ) )
36 velsn 4193 . . . . . . . . . 10 |- ( z e. { x } <-> z = x )
3736anbi1i 731 . . . . . . . . 9 |- ( ( z e. { x } /\ ( y e. B /\ <. y , z >. e. R ) ) <-> ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) )
3834, 35, 373bitri 286 . . . . . . . 8 |- ( ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) <-> ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) )
3938exbii 1774 . . . . . . 7 |- ( E. z ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) <-> E. z ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) )
40 vex 3203 . . . . . . . 8 |- x e. _V
41 opeq2 4403 . . . . . . . . . 10 |- ( z = x -> <. y , z >. = <. y , x >. )
4241eleq1d 2686 . . . . . . . . 9 |- ( z = x -> ( <. y , z >. e. R <-> <. y , x >. e. R ) )
4342anbi2d 740 . . . . . . . 8 |- ( z = x -> ( ( y e. B /\ <. y , z >. e. R ) <-> ( y e. B /\ <. y , x >. e. R ) ) )
4440, 43ceqsexv 3242 . . . . . . 7 |- ( E. z ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) <-> ( y e. B /\ <. y , x >. e. R ) )
4533, 39, 443bitri 286 . . . . . 6 |- ( E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> ( y e. B /\ <. y , x >. e. R ) )
4645exbii 1774 . . . . 5 |- ( E. y E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> E. y ( y e. B /\ <. y , x >. e. R ) )
4721, 28, 463bitri 286 . . . 4 |- ( E. p p e. ( R i^i ( B X. { x } ) ) <-> E. y ( y e. B /\ <. y , x >. e. R ) )
48 n0 3931 . . . 4 |- ( ( R i^i ( B X. { x } ) ) =/= (/) <-> E. p p e. ( R i^i ( B X. { x } ) ) )
4940elima3 5473 . . . 4 |- ( x e. ( R " B ) <-> E. y ( y e. B /\ <. y , x >. e. R ) )
5047, 48, 493bitr4ri 293 . . 3 |- ( x e. ( R " B ) <-> ( R i^i ( B X. { x } ) ) =/= (/) )
5111, 15, 50vtoclbg 3267 . 2 |- ( A e. _V -> ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) ) )
521, 10, 51pm5.21nii 368 1 |- ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) )
Colors of variables: wff setvar class
Syntax hints:   <-> wb 196   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   _Vcvv 3200   i^i cin 3573   (/)c0 3915   {csn 4177   <.cop 4183   X. cxp 5112   "cima 5117
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator