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

Metamath Proof Explorer

Theorem xpsfrnel2

Description: Elementhood in the target space of the function F appearing in xpsval . (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Assertion xpsfrnel2 
|- ( { <. (/) , X >. , <. 1o , Y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) )

Proof

Step Hyp Ref Expression
1 xpsfrnel 
 |-  ( { <. (/) , X >. , <. 1o , Y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) )
2 fnpr2ob 
 |-  ( ( X e. _V /\ Y e. _V ) <-> { <. (/) , X >. , <. 1o , Y >. } Fn 2o )
3 2 biimpri 
 |-  ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o -> ( X e. _V /\ Y e. _V ) )
4 3 3ad2ant1 
 |-  ( ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) -> ( X e. _V /\ Y e. _V ) )
5 elex 
 |-  ( X e. A -> X e. _V )
6 elex 
 |-  ( Y e. B -> Y e. _V )
7 5 6 anim12i 
 |-  ( ( X e. A /\ Y e. B ) -> ( X e. _V /\ Y e. _V ) )
8 3anass 
 |-  ( ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) <-> ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) ) )
9 fnpr2o 
 |-  ( ( X e. _V /\ Y e. _V ) -> { <. (/) , X >. , <. 1o , Y >. } Fn 2o )
10 9 biantrurd 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) <-> ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) ) ) )
11 fvpr0o 
 |-  ( X e. _V -> ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) = X )
12 11 eleq1d 
 |-  ( X e. _V -> ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A <-> X e. A ) )
13 fvpr1o 
 |-  ( Y e. _V -> ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) = Y )
14 13 eleq1d 
 |-  ( Y e. _V -> ( ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B <-> Y e. B ) )
15 12 14 bi2anan9 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) <-> ( X e. A /\ Y e. B ) ) )
16 10 15 bitr3d 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) ) <-> ( X e. A /\ Y e. B ) ) )
17 8 16 bitrid 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) <-> ( X e. A /\ Y e. B ) ) )
18 4 7 17 pm5.21nii 
 |-  ( ( { <. (/) , X >. , <. 1o , Y >. } Fn 2o /\ ( { <. (/) , X >. , <. 1o , Y >. } ` (/) ) e. A /\ ( { <. (/) , X >. , <. 1o , Y >. } ` 1o ) e. B ) <-> ( X e. A /\ Y e. B ) )
19 1 18 bitri 
 |-  ( { <. (/) , X >. , <. 1o , Y >. } e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( X e. A /\ Y e. B ) )