Metamath Proof Explorer


Theorem f1prex

Description: Relate a one-to-one function with a pair as domain and two different variables. (Contributed by Thierry Arnoux, 12-Jul-2020)

Ref Expression
Hypotheses f1prex.1 x = f A ψ χ
f1prex.2 y = f B χ φ
Assertion f1prex A V B W A B f f : A B 1-1 D φ x D y D x y ψ

Proof

Step Hyp Ref Expression
1 f1prex.1 x = f A ψ χ
2 f1prex.2 y = f B χ φ
3 simpl1 A V B W A B f : A B 1-1 D φ A V
4 simpl2 A V B W A B f : A B 1-1 D φ B W
5 simprl A V B W A B f : A B 1-1 D φ f : A B 1-1 D
6 f1f f : A B 1-1 D f : A B D
7 5 6 syl A V B W A B f : A B 1-1 D φ f : A B D
8 fpr2g A V B W f : A B D f A D f B D f = A f A B f B
9 8 biimpa A V B W f : A B D f A D f B D f = A f A B f B
10 9 simp1d A V B W f : A B D f A D
11 3 4 7 10 syl21anc A V B W A B f : A B 1-1 D φ f A D
12 9 simp2d A V B W f : A B D f B D
13 3 4 7 12 syl21anc A V B W A B f : A B 1-1 D φ f B D
14 prid1g A V A A B
15 3 14 syl A V B W A B f : A B 1-1 D φ A A B
16 prid2g B W B A B
17 4 16 syl A V B W A B f : A B 1-1 D φ B A B
18 15 17 jca A V B W A B f : A B 1-1 D φ A A B B A B
19 simpl3 A V B W A B f : A B 1-1 D φ A B
20 f1veqaeq f : A B 1-1 D A A B B A B f A = f B A = B
21 20 necon3d f : A B 1-1 D A A B B A B A B f A f B
22 21 imp f : A B 1-1 D A A B B A B A B f A f B
23 5 18 19 22 syl21anc A V B W A B f : A B 1-1 D φ f A f B
24 simprr A V B W A B f : A B 1-1 D φ φ
25 23 24 jca A V B W A B f : A B 1-1 D φ f A f B φ
26 neeq1 x = f A x y f A y
27 26 1 anbi12d x = f A x y ψ f A y χ
28 neeq2 y = f B f A y f A f B
29 28 2 anbi12d y = f B f A y χ f A f B φ
30 27 29 rspc2ev f A D f B D f A f B φ x D y D x y ψ
31 11 13 25 30 syl3anc A V B W A B f : A B 1-1 D φ x D y D x y ψ
32 31 ex A V B W A B f : A B 1-1 D φ x D y D x y ψ
33 32 exlimdv A V B W A B f f : A B 1-1 D φ x D y D x y ψ
34 simpll1 A V B W A B x D y D x y ψ A V
35 simplrl A V B W A B x D y D x y ψ x D
36 34 35 jca A V B W A B x D y D x y ψ A V x D
37 simpll2 A V B W A B x D y D x y ψ B W
38 simplrr A V B W A B x D y D x y ψ y D
39 37 38 jca A V B W A B x D y D x y ψ B W y D
40 simpll3 A V B W A B x D y D x y ψ A B
41 simprl A V B W A B x D y D x y ψ x y
42 f1oprg A V x D B W y D A B x y A x B y : A B 1-1 onto x y
43 42 imp A V x D B W y D A B x y A x B y : A B 1-1 onto x y
44 36 39 40 41 43 syl22anc A V B W A B x D y D x y ψ A x B y : A B 1-1 onto x y
45 f1of1 A x B y : A B 1-1 onto x y A x B y : A B 1-1 x y
46 44 45 syl A V B W A B x D y D x y ψ A x B y : A B 1-1 x y
47 35 38 prssd A V B W A B x D y D x y ψ x y D
48 f1ss A x B y : A B 1-1 x y x y D A x B y : A B 1-1 D
49 46 47 48 syl2anc A V B W A B x D y D x y ψ A x B y : A B 1-1 D
50 fvpr1g A V x D A B A x B y A = x
51 50 eqcomd A V x D A B x = A x B y A
52 34 35 40 51 syl3anc A V B W A B x D y D x y ψ x = A x B y A
53 fvpr2g B W y D A B A x B y B = y
54 53 eqcomd B W y D A B y = A x B y B
55 37 38 40 54 syl3anc A V B W A B x D y D x y ψ y = A x B y B
56 prex A x B y V
57 f1eq1 f = A x B y f : A B 1-1 D A x B y : A B 1-1 D
58 fveq1 f = A x B y f A = A x B y A
59 58 eqeq2d f = A x B y x = f A x = A x B y A
60 fveq1 f = A x B y f B = A x B y B
61 60 eqeq2d f = A x B y y = f B y = A x B y B
62 59 61 anbi12d f = A x B y x = f A y = f B x = A x B y A y = A x B y B
63 57 62 anbi12d f = A x B y f : A B 1-1 D x = f A y = f B A x B y : A B 1-1 D x = A x B y A y = A x B y B
64 56 63 spcev A x B y : A B 1-1 D x = A x B y A y = A x B y B f f : A B 1-1 D x = f A y = f B
65 49 52 55 64 syl12anc A V B W A B x D y D x y ψ f f : A B 1-1 D x = f A y = f B
66 simprl A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B f : A B 1-1 D
67 simplrr A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B ψ
68 simprrl A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B x = f A
69 68 1 syl A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B ψ χ
70 67 69 mpbid A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B χ
71 simprrr A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B y = f B
72 71 2 syl A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B χ φ
73 70 72 mpbid A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B φ
74 66 73 jca A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B f : A B 1-1 D φ
75 74 ex A V B W A B x D y D x y ψ f : A B 1-1 D x = f A y = f B f : A B 1-1 D φ
76 75 eximdv A V B W A B x D y D x y ψ f f : A B 1-1 D x = f A y = f B f f : A B 1-1 D φ
77 65 76 mpd A V B W A B x D y D x y ψ f f : A B 1-1 D φ
78 77 ex A V B W A B x D y D x y ψ f f : A B 1-1 D φ
79 78 rexlimdvva A V B W A B x D y D x y ψ f f : A B 1-1 D φ
80 33 79 impbid A V B W A B f f : A B 1-1 D φ x D y D x y ψ