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

Metamath Proof Explorer

Theorem elixp2

Description: Membership in an infinite Cartesian product. See df-ixp for discussion of the notation. (Contributed by NM, 28-Sep-2006)

Ref Expression
Assertion elixp2 
|- ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )

Proof

Step Hyp Ref Expression
1 fneq1 
 |-  ( f = F -> ( f Fn A <-> F Fn A ) )
2 fveq1 
 |-  ( f = F -> ( f ` x ) = ( F ` x ) )
3 2 eleq1d 
 |-  ( f = F -> ( ( f ` x ) e. B <-> ( F ` x ) e. B ) )
4 3 ralbidv 
 |-  ( f = F -> ( A. x e. A ( f ` x ) e. B <-> A. x e. A ( F ` x ) e. B ) )
5 1 4 anbi12d 
 |-  ( f = F -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. B ) <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
6 dfixp 
 |-  X_ x e. A B = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. B ) }
7 5 6 elab2g 
 |-  ( F e. _V -> ( F e. X_ x e. A B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
8 7 pm5.32i 
 |-  ( ( F e. _V /\ F e. X_ x e. A B ) <-> ( F e. _V /\ ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
9 elex 
 |-  ( F e. X_ x e. A B -> F e. _V )
10 9 pm4.71ri 
 |-  ( F e. X_ x e. A B <-> ( F e. _V /\ F e. X_ x e. A B ) )
11 3anass 
 |-  ( ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) <-> ( F e. _V /\ ( F Fn A /\ A. x e. A ( F ` x ) e. B ) ) )
12 8 10 11 3bitr4i 
 |-  ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )