Metamath Proof Explorer

Theorem imainss

Description: An upper bound for intersection with an image. Theorem 41 of Suppes p. 66. (Contributed by NM, 11-Aug-2004)

Ref Expression
Assertion imainss 
|- ( ( R " A ) i^i B ) C_ ( R " ( A i^i ( `' R " B ) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 vex 
 |-  x e. _V
3 1 2 brcnv 
 |-  ( y `' R x <-> x R y )
4 19.8a 
 |-  ( ( y e. B /\ y `' R x ) -> E. y ( y e. B /\ y `' R x ) )
5 3 4 sylan2br 
 |-  ( ( y e. B /\ x R y ) -> E. y ( y e. B /\ y `' R x ) )
6 5 ancoms 
 |-  ( ( x R y /\ y e. B ) -> E. y ( y e. B /\ y `' R x ) )
7 6 anim2i 
 |-  ( ( x e. A /\ ( x R y /\ y e. B ) ) -> ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) )
8 simprl 
 |-  ( ( x e. A /\ ( x R y /\ y e. B ) ) -> x R y )
9 7 8 jca 
 |-  ( ( x e. A /\ ( x R y /\ y e. B ) ) -> ( ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) /\ x R y ) )
10 9 anassrs 
 |-  ( ( ( x e. A /\ x R y ) /\ y e. B ) -> ( ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) /\ x R y ) )
11 elin 
 |-  ( x e. ( A i^i ( `' R " B ) ) <-> ( x e. A /\ x e. ( `' R " B ) ) )
12 2 elima2 
 |-  ( x e. ( `' R " B ) <-> E. y ( y e. B /\ y `' R x ) )
13 12 anbi2i 
 |-  ( ( x e. A /\ x e. ( `' R " B ) ) <-> ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) )
14 11 13 bitri 
 |-  ( x e. ( A i^i ( `' R " B ) ) <-> ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) )
15 14 anbi1i 
 |-  ( ( x e. ( A i^i ( `' R " B ) ) /\ x R y ) <-> ( ( x e. A /\ E. y ( y e. B /\ y `' R x ) ) /\ x R y ) )
16 10 15 sylibr 
 |-  ( ( ( x e. A /\ x R y ) /\ y e. B ) -> ( x e. ( A i^i ( `' R " B ) ) /\ x R y ) )
17 16 eximi 
 |-  ( E. x ( ( x e. A /\ x R y ) /\ y e. B ) -> E. x ( x e. ( A i^i ( `' R " B ) ) /\ x R y ) )
18 1 elima2 
 |-  ( y e. ( R " A ) <-> E. x ( x e. A /\ x R y ) )
19 18 anbi1i 
 |-  ( ( y e. ( R " A ) /\ y e. B ) <-> ( E. x ( x e. A /\ x R y ) /\ y e. B ) )
20 elin 
 |-  ( y e. ( ( R " A ) i^i B ) <-> ( y e. ( R " A ) /\ y e. B ) )
21 19.41v 
 |-  ( E. x ( ( x e. A /\ x R y ) /\ y e. B ) <-> ( E. x ( x e. A /\ x R y ) /\ y e. B ) )
22 19 20 21 3bitr4i 
 |-  ( y e. ( ( R " A ) i^i B ) <-> E. x ( ( x e. A /\ x R y ) /\ y e. B ) )
23 1 elima2 
 |-  ( y e. ( R " ( A i^i ( `' R " B ) ) ) <-> E. x ( x e. ( A i^i ( `' R " B ) ) /\ x R y ) )
24 17 22 23 3imtr4i 
 |-  ( y e. ( ( R " A ) i^i B ) -> y e. ( R " ( A i^i ( `' R " B ) ) ) )
25 24 ssriv 
 |-  ( ( R " A ) i^i B ) C_ ( R " ( A i^i ( `' R " B ) ) )