Metamath Proof Explorer

Theorem elintima

Description: Element of intersection of images. (Contributed by RP, 13-Apr-2020)

Ref Expression
Assertion elintima 
|- ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 1 elint2 
 |-  ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. z e. { x | E. a e. A x = ( a " B ) } y e. z )
3 elequ2 
 |-  ( z = x -> ( y e. z <-> y e. x ) )
4 3 ralab2 
 |-  ( A. z e. { x | E. a e. A x = ( a " B ) } y e. z <-> A. x ( E. a e. A x = ( a " B ) -> y e. x ) )
5 df-rex 
 |-  ( E. a e. A x = ( a " B ) <-> E. a ( a e. A /\ x = ( a " B ) ) )
6 5 imbi1i 
 |-  ( ( E. a e. A x = ( a " B ) -> y e. x ) <-> ( E. a ( a e. A /\ x = ( a " B ) ) -> y e. x ) )
7 19.23v 
 |-  ( A. a ( ( a e. A /\ x = ( a " B ) ) -> y e. x ) <-> ( E. a ( a e. A /\ x = ( a " B ) ) -> y e. x ) )
8 simpr 
 |-  ( ( a e. A /\ x = ( a " B ) ) -> x = ( a " B ) )
9 8 eleq2d 
 |-  ( ( a e. A /\ x = ( a " B ) ) -> ( y e. x <-> y e. ( a " B ) ) )
10 9 pm5.74i 
 |-  ( ( ( a e. A /\ x = ( a " B ) ) -> y e. x ) <-> ( ( a e. A /\ x = ( a " B ) ) -> y e. ( a " B ) ) )
11 1 elima 
 |-  ( y e. ( a " B ) <-> E. b e. B b a y )
12 df-br 
 |-  ( b a y <-> <. b , y >. e. a )
13 12 rexbii 
 |-  ( E. b e. B b a y <-> E. b e. B <. b , y >. e. a )
14 11 13 bitri 
 |-  ( y e. ( a " B ) <-> E. b e. B <. b , y >. e. a )
15 14 imbi2i 
 |-  ( ( ( a e. A /\ x = ( a " B ) ) -> y e. ( a " B ) ) <-> ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
16 10 15 bitri 
 |-  ( ( ( a e. A /\ x = ( a " B ) ) -> y e. x ) <-> ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
17 16 albii 
 |-  ( A. a ( ( a e. A /\ x = ( a " B ) ) -> y e. x ) <-> A. a ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
18 6 7 17 3bitr2i 
 |-  ( ( E. a e. A x = ( a " B ) -> y e. x ) <-> A. a ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
19 18 albii 
 |-  ( A. x ( E. a e. A x = ( a " B ) -> y e. x ) <-> A. x A. a ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
20 19.23v 
 |-  ( A. x ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> ( E. x ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
21 vex 
 |-  a e. _V
22 21 imaex 
 |-  ( a " B ) e. _V
23 22 isseti 
 |-  E. x x = ( a " B )
24 19.42v 
 |-  ( E. x ( a e. A /\ x = ( a " B ) ) <-> ( a e. A /\ E. x x = ( a " B ) ) )
25 23 24 mpbiran2 
 |-  ( E. x ( a e. A /\ x = ( a " B ) ) <-> a e. A )
26 25 imbi1i 
 |-  ( ( E. x ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> ( a e. A -> E. b e. B <. b , y >. e. a ) )
27 20 26 bitri 
 |-  ( A. x ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> ( a e. A -> E. b e. B <. b , y >. e. a ) )
28 27 albii 
 |-  ( A. a A. x ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> A. a ( a e. A -> E. b e. B <. b , y >. e. a ) )
29 alcom 
 |-  ( A. x A. a ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> A. a A. x ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) )
30 df-ral 
 |-  ( A. a e. A E. b e. B <. b , y >. e. a <-> A. a ( a e. A -> E. b e. B <. b , y >. e. a ) )
31 28 29 30 3bitr4i 
 |-  ( A. x A. a ( ( a e. A /\ x = ( a " B ) ) -> E. b e. B <. b , y >. e. a ) <-> A. a e. A E. b e. B <. b , y >. e. a )
32 19 31 bitri 
 |-  ( A. x ( E. a e. A x = ( a " B ) -> y e. x ) <-> A. a e. A E. b e. B <. b , y >. e. a )
33 4 32 bitri 
 |-  ( A. z e. { x | E. a e. A x = ( a " B ) } y e. z <-> A. a e. A E. b e. B <. b , y >. e. a )
34 2 33 bitri 
 |-  ( y e. |^| { x | E. a e. A x = ( a " B ) } <-> A. a e. A E. b e. B <. b , y >. e. a )