Metamath Proof Explorer

Theorem elima4

Description: Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018)

Ref Expression
Assertion elima4 
|- ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. ( R " B ) -> A e. _V )
2 xpeq2 
 |-  ( { A } = (/) -> ( B X. { A } ) = ( B X. (/) ) )
3 xp0 
 |-  ( B X. (/) ) = (/)
4 2 3 eqtrdi 
 |-  ( { A } = (/) -> ( B X. { A } ) = (/) )
5 4 ineq2d 
 |-  ( { A } = (/) -> ( R i^i ( B X. { A } ) ) = ( R i^i (/) ) )
6 in0 
 |-  ( R i^i (/) ) = (/)
7 5 6 eqtrdi 
 |-  ( { A } = (/) -> ( R i^i ( B X. { A } ) ) = (/) )
8 7 necon3i 
 |-  ( ( R i^i ( B X. { A } ) ) =/= (/) -> { A } =/= (/) )
9 snnzb 
 |-  ( A e. _V <-> { A } =/= (/) )
10 8 9 sylibr 
 |-  ( ( R i^i ( B X. { A } ) ) =/= (/) -> A e. _V )
11 eleq1 
 |-  ( x = A -> ( x e. ( R " B ) <-> A e. ( R " B ) ) )
12 sneq 
 |-  ( x = A -> { x } = { A } )
13 12 xpeq2d 
 |-  ( x = A -> ( B X. { x } ) = ( B X. { A } ) )
14 13 ineq2d 
 |-  ( x = A -> ( R i^i ( B X. { x } ) ) = ( R i^i ( B X. { A } ) ) )
15 14 neeq1d 
 |-  ( x = A -> ( ( R i^i ( B X. { x } ) ) =/= (/) <-> ( R i^i ( B X. { A } ) ) =/= (/) ) )
16 elin 
 |-  ( p e. ( R i^i ( B X. { x } ) ) <-> ( p e. R /\ p e. ( B X. { x } ) ) )
17 ancom 
 |-  ( ( p e. R /\ p e. ( B X. { x } ) ) <-> ( p e. ( B X. { x } ) /\ p e. R ) )
18 elxp 
 |-  ( p e. ( B X. { x } ) <-> E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) )
19 18 anbi1i 
 |-  ( ( p e. ( B X. { x } ) /\ p e. R ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
20 16 17 19 3bitri 
 |-  ( p e. ( R i^i ( B X. { x } ) ) <-> ( E. y E. z ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) )
21 20 exbii 
 |-  ( 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 
 |-  ( ( ( p = <. y , z >. /\ ( y e. B /\ z e. { x } ) ) /\ p e. R ) <-> ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) )
23 22 2exbii 
 |-  ( 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 
 |-  ( 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 ) )
25 23 24 bitr3i 
 |-  ( 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 ) )
26 25 exbii 
 |-  ( 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 
 |-  ( 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 ) ) )
28 26 27 bitr3i 
 |-  ( 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 
 |-  <. y , z >. e. _V
30 eleq1 
 |-  ( p = <. y , z >. -> ( p e. R <-> <. y , z >. e. R ) )
31 30 anbi2d 
 |-  ( p = <. y , z >. -> ( ( ( y e. B /\ z e. { x } ) /\ p e. R ) <-> ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) ) )
32 29 31 ceqsexv 
 |-  ( E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) )
33 32 exbii 
 |-  ( 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 
 |-  ( ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) <-> ( y e. B /\ ( z e. { x } /\ <. y , z >. e. R ) ) )
35 an12 
 |-  ( ( y e. B /\ ( z e. { x } /\ <. y , z >. e. R ) ) <-> ( z e. { x } /\ ( y e. B /\ <. y , z >. e. R ) ) )
36 velsn 
 |-  ( z e. { x } <-> z = x )
37 36 anbi1i 
 |-  ( ( z e. { x } /\ ( y e. B /\ <. y , z >. e. R ) ) <-> ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) )
38 34 35 37 3bitri 
 |-  ( ( ( y e. B /\ z e. { x } ) /\ <. y , z >. e. R ) <-> ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) )
39 38 exbii 
 |-  ( 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 
 |-  x e. _V
41 opeq2 
 |-  ( z = x -> <. y , z >. = <. y , x >. )
42 41 eleq1d 
 |-  ( z = x -> ( <. y , z >. e. R <-> <. y , x >. e. R ) )
43 42 anbi2d 
 |-  ( z = x -> ( ( y e. B /\ <. y , z >. e. R ) <-> ( y e. B /\ <. y , x >. e. R ) ) )
44 40 43 ceqsexv 
 |-  ( E. z ( z = x /\ ( y e. B /\ <. y , z >. e. R ) ) <-> ( y e. B /\ <. y , x >. e. R ) )
45 33 39 44 3bitri 
 |-  ( E. z E. p ( p = <. y , z >. /\ ( ( y e. B /\ z e. { x } ) /\ p e. R ) ) <-> ( y e. B /\ <. y , x >. e. R ) )
46 45 exbii 
 |-  ( 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 ) )
47 21 28 46 3bitri 
 |-  ( E. p p e. ( R i^i ( B X. { x } ) ) <-> E. y ( y e. B /\ <. y , x >. e. R ) )
48 n0 
 |-  ( ( R i^i ( B X. { x } ) ) =/= (/) <-> E. p p e. ( R i^i ( B X. { x } ) ) )
49 40 elima3 
 |-  ( x e. ( R " B ) <-> E. y ( y e. B /\ <. y , x >. e. R ) )
50 47 48 49 3bitr4ri 
 |-  ( x e. ( R " B ) <-> ( R i^i ( B X. { x } ) ) =/= (/) )
51 11 15 50 vtoclbg 
 |-  ( A e. _V -> ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) ) )
52 1 10 51 pm5.21nii 
 |-  ( A e. ( R " B ) <-> ( R i^i ( B X. { A } ) ) =/= (/) )