Metamath Proof Explorer

Theorem ixpf

Description: A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion ixpf 
|- ( F e. X_ x e. A B -> F : A --> U_ x e. A B )

Proof

Step Hyp Ref Expression
1 elixp2 
 |-  ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
2 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
3 2 sseld 
 |-  ( x e. A -> ( ( F ` x ) e. B -> ( F ` x ) e. U_ x e. A B ) )
4 3 ralimia 
 |-  ( A. x e. A ( F ` x ) e. B -> A. x e. A ( F ` x ) e. U_ x e. A B )
5 4 anim2i 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ( F Fn A /\ A. x e. A ( F ` x ) e. U_ x e. A B ) )
6 nfcv 
 |-  F/_ x A
7 nfiu1 
 |-  F/_ x U_ x e. A B
8 nfcv 
 |-  F/_ x F
9 6 7 8 ffnfvf 
 |-  ( F : A --> U_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. U_ x e. A B ) )
10 5 9 sylibr 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> U_ x e. A B )
11 10 3adant1 
 |-  ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) -> F : A --> U_ x e. A B )
12 1 11 sylbi 
 |-  ( F e. X_ x e. A B -> F : A --> U_ x e. A B )