Metamath Proof Explorer

Theorem xpsfrnel

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

Ref Expression
Assertion xpsfrnel 
|- ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )

Proof

Step Hyp Ref Expression
1 elixp2 
 |-  ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G e. _V /\ G Fn 2o /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) )
2 3ancoma 
 |-  ( ( G e. _V /\ G Fn 2o /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) <-> ( G Fn 2o /\ G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) )
3 2onn 
 |-  2o e. _om
4 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
5 3 4 ax-mp 
 |-  2o e. Fin
6 fnfi 
 |-  ( ( G Fn 2o /\ 2o e. Fin ) -> G e. Fin )
7 5 6 mpan2 
 |-  ( G Fn 2o -> G e. Fin )
8 7 elexd 
 |-  ( G Fn 2o -> G e. _V )
9 8 biantrurd 
 |-  ( G Fn 2o -> ( A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) <-> ( G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) ) )
10 df2o3 
 |-  2o = { (/) , 1o }
11 10 raleqi 
 |-  ( A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) <-> A. k e. { (/) , 1o } ( G ` k ) e. if ( k = (/) , A , B ) )
12 0ex 
 |-  (/) e. _V
13 1oex 
 |-  1o e. _V
14 fveq2 
 |-  ( k = (/) -> ( G ` k ) = ( G ` (/) ) )
15 iftrue 
 |-  ( k = (/) -> if ( k = (/) , A , B ) = A )
16 14 15 eleq12d 
 |-  ( k = (/) -> ( ( G ` k ) e. if ( k = (/) , A , B ) <-> ( G ` (/) ) e. A ) )
17 fveq2 
 |-  ( k = 1o -> ( G ` k ) = ( G ` 1o ) )
18 1n0 
 |-  1o =/= (/)
19 neeq1 
 |-  ( k = 1o -> ( k =/= (/) <-> 1o =/= (/) ) )
20 18 19 mpbiri 
 |-  ( k = 1o -> k =/= (/) )
21 ifnefalse 
 |-  ( k =/= (/) -> if ( k = (/) , A , B ) = B )
22 20 21 syl 
 |-  ( k = 1o -> if ( k = (/) , A , B ) = B )
23 17 22 eleq12d 
 |-  ( k = 1o -> ( ( G ` k ) e. if ( k = (/) , A , B ) <-> ( G ` 1o ) e. B ) )
24 12 13 16 23 ralpr 
 |-  ( A. k e. { (/) , 1o } ( G ` k ) e. if ( k = (/) , A , B ) <-> ( ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
25 11 24 bitri 
 |-  ( A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) <-> ( ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
26 9 25 bitr3di 
 |-  ( G Fn 2o -> ( ( G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) <-> ( ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) ) )
27 26 pm5.32i 
 |-  ( ( G Fn 2o /\ ( G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) ) <-> ( G Fn 2o /\ ( ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) ) )
28 3anass 
 |-  ( ( G Fn 2o /\ G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) <-> ( G Fn 2o /\ ( G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) ) )
29 3anass 
 |-  ( ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) <-> ( G Fn 2o /\ ( ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) ) )
30 27 28 29 3bitr4i 
 |-  ( ( G Fn 2o /\ G e. _V /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
31 2 30 bitri 
 |-  ( ( G e. _V /\ G Fn 2o /\ A. k e. 2o ( G ` k ) e. if ( k = (/) , A , B ) ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )
32 1 31 bitri 
 |-  ( G e. X_ k e. 2o if ( k = (/) , A , B ) <-> ( G Fn 2o /\ ( G ` (/) ) e. A /\ ( G ` 1o ) e. B ) )