Metamath Proof Explorer


Theorem xpdom2

Description: Dominance law for Cartesian product. Proposition 10.33(2) of TakeutiZaring p. 92. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypothesis xpdom.2 C V
Assertion xpdom2 A B C × A C × B

Proof

Step Hyp Ref Expression
1 xpdom.2 C V
2 brdomi A B f f : A 1-1 B
3 f1f f : A 1-1 B f : A B
4 ffvelrn f : A B ran x A f ran x B
5 4 ex f : A B ran x A f ran x B
6 3 5 syl f : A 1-1 B ran x A f ran x B
7 6 anim2d f : A 1-1 B dom x C ran x A dom x C f ran x B
8 7 adantld f : A 1-1 B x = dom x ran x dom x C ran x A dom x C f ran x B
9 elxp4 x C × A x = dom x ran x dom x C ran x A
10 opelxp dom x f ran x C × B dom x C f ran x B
11 8 9 10 3imtr4g f : A 1-1 B x C × A dom x f ran x C × B
12 11 adantl A B f : A 1-1 B x C × A dom x f ran x C × B
13 elxp2 x C × A z C w A x = z w
14 elxp2 y C × A v C u A y = v u
15 vex z V
16 fvex f w V
17 15 16 opth z f w = v f u z = v f w = f u
18 f1fveq f : A 1-1 B w A u A f w = f u w = u
19 18 ancoms w A u A f : A 1-1 B f w = f u w = u
20 19 anbi2d w A u A f : A 1-1 B z = v f w = f u z = v w = u
21 17 20 syl5bb w A u A f : A 1-1 B z f w = v f u z = v w = u
22 21 ex w A u A f : A 1-1 B z f w = v f u z = v w = u
23 22 ad2ant2l z C w A v C u A f : A 1-1 B z f w = v f u z = v w = u
24 23 imp z C w A v C u A f : A 1-1 B z f w = v f u z = v w = u
25 24 adantlr z C w A v C u A x = z w y = v u f : A 1-1 B z f w = v f u z = v w = u
26 sneq x = z w x = z w
27 26 dmeqd x = z w dom x = dom z w
28 27 unieqd x = z w dom x = dom z w
29 vex w V
30 15 29 op1sta dom z w = z
31 28 30 eqtrdi x = z w dom x = z
32 26 rneqd x = z w ran x = ran z w
33 32 unieqd x = z w ran x = ran z w
34 15 29 op2nda ran z w = w
35 33 34 eqtrdi x = z w ran x = w
36 35 fveq2d x = z w f ran x = f w
37 31 36 opeq12d x = z w dom x f ran x = z f w
38 sneq y = v u y = v u
39 38 dmeqd y = v u dom y = dom v u
40 39 unieqd y = v u dom y = dom v u
41 vex v V
42 vex u V
43 41 42 op1sta dom v u = v
44 40 43 eqtrdi y = v u dom y = v
45 38 rneqd y = v u ran y = ran v u
46 45 unieqd y = v u ran y = ran v u
47 41 42 op2nda ran v u = u
48 46 47 eqtrdi y = v u ran y = u
49 48 fveq2d y = v u f ran y = f u
50 44 49 opeq12d y = v u dom y f ran y = v f u
51 37 50 eqeqan12d x = z w y = v u dom x f ran x = dom y f ran y z f w = v f u
52 51 ad2antlr z C w A v C u A x = z w y = v u f : A 1-1 B dom x f ran x = dom y f ran y z f w = v f u
53 eqeq12 x = z w y = v u x = y z w = v u
54 15 29 opth z w = v u z = v w = u
55 53 54 bitrdi x = z w y = v u x = y z = v w = u
56 55 ad2antlr z C w A v C u A x = z w y = v u f : A 1-1 B x = y z = v w = u
57 25 52 56 3bitr4d z C w A v C u A x = z w y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
58 57 exp53 z C w A v C u A x = z w y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
59 58 com23 z C w A x = z w v C u A y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
60 59 rexlimivv z C w A x = z w v C u A y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
61 60 rexlimdvv z C w A x = z w v C u A y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
62 61 imp z C w A x = z w v C u A y = v u f : A 1-1 B dom x f ran x = dom y f ran y x = y
63 13 14 62 syl2anb x C × A y C × A f : A 1-1 B dom x f ran x = dom y f ran y x = y
64 63 com12 f : A 1-1 B x C × A y C × A dom x f ran x = dom y f ran y x = y
65 64 adantl A B f : A 1-1 B x C × A y C × A dom x f ran x = dom y f ran y x = y
66 reldom Rel
67 66 brrelex1i A B A V
68 xpexg C V A V C × A V
69 1 67 68 sylancr A B C × A V
70 69 adantr A B f : A 1-1 B C × A V
71 66 brrelex2i A B B V
72 xpexg C V B V C × B V
73 1 71 72 sylancr A B C × B V
74 73 adantr A B f : A 1-1 B C × B V
75 12 65 70 74 dom3d A B f : A 1-1 B C × A C × B
76 2 75 exlimddv A B C × A C × B