Metamath Proof Explorer

Theorem rexunirn

Description: Restricted existential quantification over the union of the range of a function. Cf. rexrn and eluni2 . (Contributed by Thierry Arnoux, 19-Sep-2017)

Ref Expression
Hypotheses rexunirn.1 
|- F = ( x e. A |-> B )
rexunirn.2 
|- ( x e. A -> B e. V )
Assertion rexunirn 
|- ( E. x e. A E. y e. B ph -> E. y e. U. ran F ph )

Proof

Step Hyp Ref Expression
1 rexunirn.1 
 |-  F = ( x e. A |-> B )
2 rexunirn.2 
 |-  ( x e. A -> B e. V )
3 df-rex 
 |-  ( E. x e. A E. y e. B ph <-> E. x ( x e. A /\ E. y e. B ph ) )
4 19.42v 
 |-  ( E. y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ E. y ( y e. B /\ ph ) ) )
5 df-rex 
 |-  ( E. y e. B ph <-> E. y ( y e. B /\ ph ) )
6 5 anbi2i 
 |-  ( ( x e. A /\ E. y e. B ph ) <-> ( x e. A /\ E. y ( y e. B /\ ph ) ) )
7 4 6 bitr4i 
 |-  ( E. y ( x e. A /\ ( y e. B /\ ph ) ) <-> ( x e. A /\ E. y e. B ph ) )
8 7 exbii 
 |-  ( E. x E. y ( x e. A /\ ( y e. B /\ ph ) ) <-> E. x ( x e. A /\ E. y e. B ph ) )
9 3 8 bitr4i 
 |-  ( E. x e. A E. y e. B ph <-> E. x E. y ( x e. A /\ ( y e. B /\ ph ) ) )
10 1 elrnmpt1 
 |-  ( ( x e. A /\ B e. V ) -> B e. ran F )
11 2 10 mpdan 
 |-  ( x e. A -> B e. ran F )
12 eleq2 
 |-  ( b = B -> ( y e. b <-> y e. B ) )
13 12 anbi1d 
 |-  ( b = B -> ( ( y e. b /\ ph ) <-> ( y e. B /\ ph ) ) )
14 13 rspcev 
 |-  ( ( B e. ran F /\ ( y e. B /\ ph ) ) -> E. b e. ran F ( y e. b /\ ph ) )
15 11 14 sylan 
 |-  ( ( x e. A /\ ( y e. B /\ ph ) ) -> E. b e. ran F ( y e. b /\ ph ) )
16 r19.41v 
 |-  ( E. b e. ran F ( y e. b /\ ph ) <-> ( E. b e. ran F y e. b /\ ph ) )
17 15 16 sylib 
 |-  ( ( x e. A /\ ( y e. B /\ ph ) ) -> ( E. b e. ran F y e. b /\ ph ) )
18 17 eximi 
 |-  ( E. y ( x e. A /\ ( y e. B /\ ph ) ) -> E. y ( E. b e. ran F y e. b /\ ph ) )
19 df-rex 
 |-  ( E. y e. U. ran F ph <-> E. y ( y e. U. ran F /\ ph ) )
20 eluni2 
 |-  ( y e. U. ran F <-> E. b e. ran F y e. b )
21 20 anbi1i 
 |-  ( ( y e. U. ran F /\ ph ) <-> ( E. b e. ran F y e. b /\ ph ) )
22 21 exbii 
 |-  ( E. y ( y e. U. ran F /\ ph ) <-> E. y ( E. b e. ran F y e. b /\ ph ) )
23 19 22 bitri 
 |-  ( E. y e. U. ran F ph <-> E. y ( E. b e. ran F y e. b /\ ph ) )
24 18 23 sylibr 
 |-  ( E. y ( x e. A /\ ( y e. B /\ ph ) ) -> E. y e. U. ran F ph )
25 24 exlimiv 
 |-  ( E. x E. y ( x e. A /\ ( y e. B /\ ph ) ) -> E. y e. U. ran F ph )
26 9 25 sylbi 
 |-  ( E. x e. A E. y e. B ph -> E. y e. U. ran F ph )