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

Metamath Proof Explorer

Theorem fprb

Description: A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013)

Ref Expression
Hypotheses fprb.1 
|- A e. _V
fprb.2 
|- B e. _V
Assertion fprb 
|- ( A =/= B -> ( F : { A , B } --> R <-> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } ) )

Proof

Step Hyp Ref Expression
1 fprb.1 
 |-  A e. _V
2 fprb.2 
 |-  B e. _V
3 1 prid1 
 |-  A e. { A , B }
4 ffvelcdm 
 |-  ( ( F : { A , B } --> R /\ A e. { A , B } ) -> ( F ` A ) e. R )
5 3 4 mpan2 
 |-  ( F : { A , B } --> R -> ( F ` A ) e. R )
6 5 adantr 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> ( F ` A ) e. R )
7 2 prid2 
 |-  B e. { A , B }
8 ffvelcdm 
 |-  ( ( F : { A , B } --> R /\ B e. { A , B } ) -> ( F ` B ) e. R )
9 7 8 mpan2 
 |-  ( F : { A , B } --> R -> ( F ` B ) e. R )
10 9 adantr 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> ( F ` B ) e. R )
11 fvex 
 |-  ( F ` A ) e. _V
12 1 11 fvpr1 
 |-  ( A =/= B -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) = ( F ` A ) )
13 fvex 
 |-  ( F ` B ) e. _V
14 2 13 fvpr2 
 |-  ( A =/= B -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) = ( F ` B ) )
15 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
16 fveq2 
 |-  ( x = A -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) )
17 15 16 eqeq12d 
 |-  ( x = A -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) <-> ( F ` A ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) ) )
18 eqcom 
 |-  ( ( F ` A ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) <-> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) = ( F ` A ) )
19 17 18 bitrdi 
 |-  ( x = A -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) <-> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) = ( F ` A ) ) )
20 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
21 fveq2 
 |-  ( x = B -> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) )
22 20 21 eqeq12d 
 |-  ( x = B -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) <-> ( F ` B ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) ) )
23 eqcom 
 |-  ( ( F ` B ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) <-> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) = ( F ` B ) )
24 22 23 bitrdi 
 |-  ( x = B -> ( ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) <-> ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) = ( F ` B ) ) )
25 1 2 19 24 ralpr 
 |-  ( A. x e. { A , B } ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) <-> ( ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` A ) = ( F ` A ) /\ ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` B ) = ( F ` B ) ) )
26 12 14 25 sylanbrc 
 |-  ( A =/= B -> A. x e. { A , B } ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) )
27 26 adantl 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> A. x e. { A , B } ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) )
28 ffn 
 |-  ( F : { A , B } --> R -> F Fn { A , B } )
29 1 2 11 13 fpr 
 |-  ( A =/= B -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } : { A , B } --> { ( F ` A ) , ( F ` B ) } )
30 29 ffnd 
 |-  ( A =/= B -> { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } Fn { A , B } )
31 eqfnfv 
 |-  ( ( F Fn { A , B } /\ { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } Fn { A , B } ) -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } <-> A. x e. { A , B } ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) ) )
32 28 30 31 syl2an 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> ( F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } <-> A. x e. { A , B } ( F ` x ) = ( { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ` x ) ) )
33 27 32 mpbird 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
34 opeq2 
 |-  ( x = ( F ` A ) -> <. A , x >. = <. A , ( F ` A ) >. )
35 34 preq1d 
 |-  ( x = ( F ` A ) -> { <. A , x >. , <. B , y >. } = { <. A , ( F ` A ) >. , <. B , y >. } )
36 35 eqeq2d 
 |-  ( x = ( F ` A ) -> ( F = { <. A , x >. , <. B , y >. } <-> F = { <. A , ( F ` A ) >. , <. B , y >. } ) )
37 opeq2 
 |-  ( y = ( F ` B ) -> <. B , y >. = <. B , ( F ` B ) >. )
38 37 preq2d 
 |-  ( y = ( F ` B ) -> { <. A , ( F ` A ) >. , <. B , y >. } = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } )
39 38 eqeq2d 
 |-  ( y = ( F ` B ) -> ( F = { <. A , ( F ` A ) >. , <. B , y >. } <-> F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) )
40 36 39 rspc2ev 
 |-  ( ( ( F ` A ) e. R /\ ( F ` B ) e. R /\ F = { <. A , ( F ` A ) >. , <. B , ( F ` B ) >. } ) -> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } )
41 6 10 33 40 syl3anc 
 |-  ( ( F : { A , B } --> R /\ A =/= B ) -> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } )
42 41 expcom 
 |-  ( A =/= B -> ( F : { A , B } --> R -> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } ) )
43 vex 
 |-  x e. _V
44 vex 
 |-  y e. _V
45 1 2 43 44 fpr 
 |-  ( A =/= B -> { <. A , x >. , <. B , y >. } : { A , B } --> { x , y } )
46 prssi 
 |-  ( ( x e. R /\ y e. R ) -> { x , y } C_ R )
47 fss 
 |-  ( ( { <. A , x >. , <. B , y >. } : { A , B } --> { x , y } /\ { x , y } C_ R ) -> { <. A , x >. , <. B , y >. } : { A , B } --> R )
48 45 46 47 syl2an 
 |-  ( ( A =/= B /\ ( x e. R /\ y e. R ) ) -> { <. A , x >. , <. B , y >. } : { A , B } --> R )
49 48 ex 
 |-  ( A =/= B -> ( ( x e. R /\ y e. R ) -> { <. A , x >. , <. B , y >. } : { A , B } --> R ) )
50 feq1 
 |-  ( F = { <. A , x >. , <. B , y >. } -> ( F : { A , B } --> R <-> { <. A , x >. , <. B , y >. } : { A , B } --> R ) )
51 50 biimprcd 
 |-  ( { <. A , x >. , <. B , y >. } : { A , B } --> R -> ( F = { <. A , x >. , <. B , y >. } -> F : { A , B } --> R ) )
52 49 51 syl6 
 |-  ( A =/= B -> ( ( x e. R /\ y e. R ) -> ( F = { <. A , x >. , <. B , y >. } -> F : { A , B } --> R ) ) )
53 52 rexlimdvv 
 |-  ( A =/= B -> ( E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } -> F : { A , B } --> R ) )
54 42 53 impbid 
 |-  ( A =/= B -> ( F : { A , B } --> R <-> E. x e. R E. y e. R F = { <. A , x >. , <. B , y >. } ) )