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 V
fprb.2 B V
Assertion fprb A B F : A B R x R y R F = A x B y

Proof

Step Hyp Ref Expression
1 fprb.1 A V
2 fprb.2 B V
3 1 prid1 A A B
4 ffvelrn F : A B R A A B F A R
5 3 4 mpan2 F : A B R F A R
6 5 adantr F : A B R A B F A R
7 2 prid2 B A B
8 ffvelrn F : A B R B A B F B R
9 7 8 mpan2 F : A B R F B R
10 9 adantr F : A B R A B F B R
11 fvex F A V
12 1 11 fvpr1 A B A F A B F B A = F A
13 fvex F B 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 x 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 x A B F x = A F A B F B x
27 26 adantl F : A B R A B x 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 x 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 x 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 R F B R F = A F A B F B x R y R F = A x B y
41 6 10 33 40 syl3anc F : A B R A B x R y R F = A x B y
42 41 expcom A B F : A B R x R y R F = A x B y
43 vex x V
44 vex y V
45 1 2 43 44 fpr A B A x B y : A B x y
46 prssi x R y R x y R
47 fss A x B y : A B x y x y R A x B y : A B R
48 45 46 47 syl2an A B x R y R A x B y : A B R
49 48 ex A B x R y 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 R y R F = A x B y F : A B R
53 52 rexlimdvv A B x R y R F = A x B y F : A B R
54 42 53 impbid A B F : A B R x R y R F = A x B y