Metamath Proof Explorer

Theorem xpwdomg

Description: Weak dominance of a Cartesian product. (Contributed by Stefan O'Rear, 13-Feb-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion xpwdomg ⊢A≼*B∧C≼*D→A×C≼*B×D

Proof

Step Hyp Ref Expression
1 brwdom3i ⊢A≼*B→∃f∀a∈A∃b∈Ba=f⁡b
2 1 adantr ⊢A≼*B∧C≼*D→∃f∀a∈A∃b∈Ba=f⁡b
3 brwdom3i ⊢C≼*D→∃g∀c∈C∃d∈Dc=g⁡d
4 3 adantl ⊢A≼*B∧C≼*D→∃g∀c∈C∃d∈Dc=g⁡d
5 relwdom ⊢Rel⁡≼*
6 5 brrelex1i ⊢A≼*B→A∈V
7 5 brrelex1i ⊢C≼*D→C∈V
8 xpexg ⊢A∈V∧C∈V→A×C∈V
9 6 7 8 syl2an ⊢A≼*B∧C≼*D→A×C∈V
10 9 adantr ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→A×C∈V
11 5 brrelex2i ⊢A≼*B→B∈V
12 5 brrelex2i ⊢C≼*D→D∈V
13 xpexg ⊢B∈V∧D∈V→B×D∈V
14 11 12 13 syl2an ⊢A≼*B∧C≼*D→B×D∈V
15 14 adantr ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→B×D∈V
16 pm3.2 ⊢∃b∈Ba=f⁡b→∃d∈Dc=g⁡d→∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d
17 16 ralimdv ⊢∃b∈Ba=f⁡b→∀c∈C∃d∈Dc=g⁡d→∀c∈C∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d
18 17 com12 ⊢∀c∈C∃d∈Dc=g⁡d→∃b∈Ba=f⁡b→∀c∈C∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d
19 18 ralimdv ⊢∀c∈C∃d∈Dc=g⁡d→∀a∈A∃b∈Ba=f⁡b→∀a∈A∀c∈C∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d
20 19 impcom ⊢∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→∀a∈A∀c∈C∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d
21 pm3.2 ⊢a=f⁡b→c=g⁡d→a=f⁡b∧c=g⁡d
22 21 reximdv ⊢a=f⁡b→∃d∈Dc=g⁡d→∃d∈Da=f⁡b∧c=g⁡d
23 22 com12 ⊢∃d∈Dc=g⁡d→a=f⁡b→∃d∈Da=f⁡b∧c=g⁡d
24 23 reximdv ⊢∃d∈Dc=g⁡d→∃b∈Ba=f⁡b→∃b∈B∃d∈Da=f⁡b∧c=g⁡d
25 24 impcom ⊢∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d→∃b∈B∃d∈Da=f⁡b∧c=g⁡d
26 25 2ralimi ⊢∀a∈A∀c∈C∃b∈Ba=f⁡b∧∃d∈Dc=g⁡d→∀a∈A∀c∈C∃b∈B∃d∈Da=f⁡b∧c=g⁡d
27 20 26 syl ⊢∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→∀a∈A∀c∈C∃b∈B∃d∈Da=f⁡b∧c=g⁡d
28 eqeq1 ⊢x=ac→x=f⁡bg⁡d↔ac=f⁡bg⁡d
29 vex ⊢a∈V
30 vex ⊢c∈V
31 29 30 opth ⊢ac=f⁡bg⁡d↔a=f⁡b∧c=g⁡d
32 28 31 bitrdi ⊢x=ac→x=f⁡bg⁡d↔a=f⁡b∧c=g⁡d
33 32 2rexbidv ⊢x=ac→∃b∈B∃d∈Dx=f⁡bg⁡d↔∃b∈B∃d∈Da=f⁡b∧c=g⁡d
34 33 ralxp ⊢∀x∈A×C∃b∈B∃d∈Dx=f⁡bg⁡d↔∀a∈A∀c∈C∃b∈B∃d∈Da=f⁡b∧c=g⁡d
35 27 34 sylibr ⊢∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→∀x∈A×C∃b∈B∃d∈Dx=f⁡bg⁡d
36 35 r19.21bi ⊢∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d∧x∈A×C→∃b∈B∃d∈Dx=f⁡bg⁡d
37 vex ⊢b∈V
38 vex ⊢d∈V
39 37 38 op1std ⊢y=bd→1st⁡y=b
40 39 fveq2d ⊢y=bd→f⁡1st⁡y=f⁡b
41 37 38 op2ndd ⊢y=bd→2nd⁡y=d
42 41 fveq2d ⊢y=bd→g⁡2nd⁡y=g⁡d
43 40 42 opeq12d ⊢y=bd→f⁡1st⁡yg⁡2nd⁡y=f⁡bg⁡d
44 43 eqeq2d ⊢y=bd→x=f⁡1st⁡yg⁡2nd⁡y↔x=f⁡bg⁡d
45 44 rexxp ⊢∃y∈B×Dx=f⁡1st⁡yg⁡2nd⁡y↔∃b∈B∃d∈Dx=f⁡bg⁡d
46 36 45 sylibr ⊢∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d∧x∈A×C→∃y∈B×Dx=f⁡1st⁡yg⁡2nd⁡y
47 46 adantll ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d∧x∈A×C→∃y∈B×Dx=f⁡1st⁡yg⁡2nd⁡y
48 10 15 47 wdom2d ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b∧∀c∈C∃d∈Dc=g⁡d→A×C≼*B×D
49 48 expr ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b→∀c∈C∃d∈Dc=g⁡d→A×C≼*B×D
50 49 exlimdv ⊢A≼*B∧C≼*D∧∀a∈A∃b∈Ba=f⁡b→∃g∀c∈C∃d∈Dc=g⁡d→A×C≼*B×D
51 50 ex ⊢A≼*B∧C≼*D→∀a∈A∃b∈Ba=f⁡b→∃g∀c∈C∃d∈Dc=g⁡d→A×C≼*B×D
52 51 exlimdv ⊢A≼*B∧C≼*D→∃f∀a∈A∃b∈Ba=f⁡b→∃g∀c∈C∃d∈Dc=g⁡d→A×C≼*B×D
53 2 4 52 mp2d ⊢A≼*B∧C≼*D→A×C≼*B×D