Metamath Proof Explorer

Theorem elunirn

Description: Membership in the union of the range of a function. See elunirnALT for a shorter proof which uses ax-pow . See elfvunirn for a more general version of the reverse direction. (Contributed by NM, 24-Sep-2006)

Ref Expression
Assertion elunirn 
|- ( Fun F -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 eluni 
 |-  ( A e. U. ran F <-> E. y ( A e. y /\ y e. ran F ) )
2 funfn 
 |-  ( Fun F <-> F Fn dom F )
3 fvelrnb 
 |-  ( F Fn dom F -> ( y e. ran F <-> E. x e. dom F ( F ` x ) = y ) )
4 2 3 sylbi 
 |-  ( Fun F -> ( y e. ran F <-> E. x e. dom F ( F ` x ) = y ) )
5 4 anbi2d 
 |-  ( Fun F -> ( ( A e. y /\ y e. ran F ) <-> ( A e. y /\ E. x e. dom F ( F ` x ) = y ) ) )
6 r19.42v 
 |-  ( E. x e. dom F ( A e. y /\ ( F ` x ) = y ) <-> ( A e. y /\ E. x e. dom F ( F ` x ) = y ) )
7 5 6 bitr4di 
 |-  ( Fun F -> ( ( A e. y /\ y e. ran F ) <-> E. x e. dom F ( A e. y /\ ( F ` x ) = y ) ) )
8 eleq2 
 |-  ( ( F ` x ) = y -> ( A e. ( F ` x ) <-> A e. y ) )
9 8 biimparc 
 |-  ( ( A e. y /\ ( F ` x ) = y ) -> A e. ( F ` x ) )
10 9 reximi 
 |-  ( E. x e. dom F ( A e. y /\ ( F ` x ) = y ) -> E. x e. dom F A e. ( F ` x ) )
11 7 10 biimtrdi 
 |-  ( Fun F -> ( ( A e. y /\ y e. ran F ) -> E. x e. dom F A e. ( F ` x ) ) )
12 11 exlimdv 
 |-  ( Fun F -> ( E. y ( A e. y /\ y e. ran F ) -> E. x e. dom F A e. ( F ` x ) ) )
13 fvelrn 
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
14 13 a1d 
 |-  ( ( Fun F /\ x e. dom F ) -> ( A e. ( F ` x ) -> ( F ` x ) e. ran F ) )
15 14 ancld 
 |-  ( ( Fun F /\ x e. dom F ) -> ( A e. ( F ` x ) -> ( A e. ( F ` x ) /\ ( F ` x ) e. ran F ) ) )
16 fvex 
 |-  ( F ` x ) e. _V
17 eleq2 
 |-  ( y = ( F ` x ) -> ( A e. y <-> A e. ( F ` x ) ) )
18 eleq1 
 |-  ( y = ( F ` x ) -> ( y e. ran F <-> ( F ` x ) e. ran F ) )
19 17 18 anbi12d 
 |-  ( y = ( F ` x ) -> ( ( A e. y /\ y e. ran F ) <-> ( A e. ( F ` x ) /\ ( F ` x ) e. ran F ) ) )
20 16 19 spcev 
 |-  ( ( A e. ( F ` x ) /\ ( F ` x ) e. ran F ) -> E. y ( A e. y /\ y e. ran F ) )
21 15 20 syl6 
 |-  ( ( Fun F /\ x e. dom F ) -> ( A e. ( F ` x ) -> E. y ( A e. y /\ y e. ran F ) ) )
22 21 rexlimdva 
 |-  ( Fun F -> ( E. x e. dom F A e. ( F ` x ) -> E. y ( A e. y /\ y e. ran F ) ) )
23 12 22 impbid 
 |-  ( Fun F -> ( E. y ( A e. y /\ y e. ran F ) <-> E. x e. dom F A e. ( F ` x ) ) )
24 1 23 bitrid 
 |-  ( Fun F -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )