This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinpreima

Description: Preimage of an intersection. (Contributed by FL, 16-Apr-2012)

Ref Expression
Assertion iinpreima 
|- ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^|_ x e. A B ) = |^|_ x e. A ( `' F " B ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> Fun F )
2 cnvimass 
 |-  ( `' F " |^|_ x e. A B ) C_ dom F
3 2 sseli 
 |-  ( y e. ( `' F " |^|_ x e. A B ) -> y e. dom F )
4 3 adantl 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> y e. dom F )
5 fvex 
 |-  ( F ` y ) e. _V
6 fvimacnvi 
 |-  ( ( Fun F /\ y e. ( `' F " |^|_ x e. A B ) ) -> ( F ` y ) e. |^|_ x e. A B )
7 6 adantlr 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> ( F ` y ) e. |^|_ x e. A B )
8 eliin 
 |-  ( ( F ` y ) e. _V -> ( ( F ` y ) e. |^|_ x e. A B <-> A. x e. A ( F ` y ) e. B ) )
9 8 biimpa 
 |-  ( ( ( F ` y ) e. _V /\ ( F ` y ) e. |^|_ x e. A B ) -> A. x e. A ( F ` y ) e. B )
10 5 7 9 sylancr 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> A. x e. A ( F ` y ) e. B )
11 fvimacnv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. B <-> y e. ( `' F " B ) ) )
12 11 ralbidv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( A. x e. A ( F ` y ) e. B <-> A. x e. A y e. ( `' F " B ) ) )
13 12 biimpa 
 |-  ( ( ( Fun F /\ y e. dom F ) /\ A. x e. A ( F ` y ) e. B ) -> A. x e. A y e. ( `' F " B ) )
14 1 4 10 13 syl21anc 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> A. x e. A y e. ( `' F " B ) )
15 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A ( `' F " B ) <-> A. x e. A y e. ( `' F " B ) ) )
16 15 elv 
 |-  ( y e. |^|_ x e. A ( `' F " B ) <-> A. x e. A y e. ( `' F " B ) )
17 14 16 sylibr 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. ( `' F " |^|_ x e. A B ) ) -> y e. |^|_ x e. A ( `' F " B ) )
18 simpll 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> Fun F )
19 15 biimpd 
 |-  ( y e. _V -> ( y e. |^|_ x e. A ( `' F " B ) -> A. x e. A y e. ( `' F " B ) ) )
20 19 elv 
 |-  ( y e. |^|_ x e. A ( `' F " B ) -> A. x e. A y e. ( `' F " B ) )
21 20 adantl 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> A. x e. A y e. ( `' F " B ) )
22 fvimacnvi 
 |-  ( ( Fun F /\ y e. ( `' F " B ) ) -> ( F ` y ) e. B )
23 22 ex 
 |-  ( Fun F -> ( y e. ( `' F " B ) -> ( F ` y ) e. B ) )
24 23 ralimdv 
 |-  ( Fun F -> ( A. x e. A y e. ( `' F " B ) -> A. x e. A ( F ` y ) e. B ) )
25 18 21 24 sylc 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> A. x e. A ( F ` y ) e. B )
26 5 8 ax-mp 
 |-  ( ( F ` y ) e. |^|_ x e. A B <-> A. x e. A ( F ` y ) e. B )
27 25 26 sylibr 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> ( F ` y ) e. |^|_ x e. A B )
28 r19.2zb 
 |-  ( A =/= (/) <-> ( A. x e. A y e. ( `' F " B ) -> E. x e. A y e. ( `' F " B ) ) )
29 28 biimpi 
 |-  ( A =/= (/) -> ( A. x e. A y e. ( `' F " B ) -> E. x e. A y e. ( `' F " B ) ) )
30 cnvimass 
 |-  ( `' F " B ) C_ dom F
31 30 sseli 
 |-  ( y e. ( `' F " B ) -> y e. dom F )
32 31 rexlimivw 
 |-  ( E. x e. A y e. ( `' F " B ) -> y e. dom F )
33 29 32 syl6 
 |-  ( A =/= (/) -> ( A. x e. A y e. ( `' F " B ) -> y e. dom F ) )
34 16 33 biimtrid 
 |-  ( A =/= (/) -> ( y e. |^|_ x e. A ( `' F " B ) -> y e. dom F ) )
35 34 adantl 
 |-  ( ( Fun F /\ A =/= (/) ) -> ( y e. |^|_ x e. A ( `' F " B ) -> y e. dom F ) )
36 35 imp 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> y e. dom F )
37 fvimacnv 
 |-  ( ( Fun F /\ y e. dom F ) -> ( ( F ` y ) e. |^|_ x e. A B <-> y e. ( `' F " |^|_ x e. A B ) ) )
38 18 36 37 syl2anc 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> ( ( F ` y ) e. |^|_ x e. A B <-> y e. ( `' F " |^|_ x e. A B ) ) )
39 27 38 mpbid 
 |-  ( ( ( Fun F /\ A =/= (/) ) /\ y e. |^|_ x e. A ( `' F " B ) ) -> y e. ( `' F " |^|_ x e. A B ) )
40 17 39 impbida 
 |-  ( ( Fun F /\ A =/= (/) ) -> ( y e. ( `' F " |^|_ x e. A B ) <-> y e. |^|_ x e. A ( `' F " B ) ) )
41 40 eqrdv 
 |-  ( ( Fun F /\ A =/= (/) ) -> ( `' F " |^|_ x e. A B ) = |^|_ x e. A ( `' F " B ) )