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 ∈ B a = f ⁡ b
2 1 adantr ⊢ A ≼ * B ∧ C ≼ * D → ∃ f ∀ a ∈ A ∃ b ∈ B a = f ⁡ b
3 brwdom3i ⊢ C ≼ * D → ∃ g ∀ c ∈ C ∃ d ∈ D c = g ⁡ d
4 3 adantl ⊢ A ≼ * B ∧ C ≼ * D → ∃ g ∀ c ∈ C ∃ d ∈ D c = 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 ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = 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 ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → B × D ∈ V
16 pm3.2 ⊢ ∃ b ∈ B a = f ⁡ b → ∃ d ∈ D c = g ⁡ d → ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d
17 16 ralimdv ⊢ ∃ b ∈ B a = f ⁡ b → ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∀ c ∈ C ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d
18 17 com12 ⊢ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∃ b ∈ B a = f ⁡ b → ∀ c ∈ C ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d
19 18 ralimdv ⊢ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d
20 19 impcom ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d
21 pm3.2 ⊢ a = f ⁡ b → c = g ⁡ d → a = f ⁡ b ∧ c = g ⁡ d
22 21 reximdv ⊢ a = f ⁡ b → ∃ d ∈ D c = g ⁡ d → ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
23 22 com12 ⊢ ∃ d ∈ D c = g ⁡ d → a = f ⁡ b → ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
24 23 reximdv ⊢ ∃ d ∈ D c = g ⁡ d → ∃ b ∈ B a = f ⁡ b → ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
25 24 impcom ⊢ ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d → ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
26 25 2ralimi ⊢ ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B a = f ⁡ b ∧ ∃ d ∈ D c = g ⁡ d → ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
27 20 26 syl ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
28 eqeq1 ⊢ x = a c → x = f ⁡ b g ⁡ d ↔ a c = f ⁡ b g ⁡ d
29 vex ⊢ a ∈ V
30 vex ⊢ c ∈ V
31 29 30 opth ⊢ a c = f ⁡ b g ⁡ d ↔ a = f ⁡ b ∧ c = g ⁡ d
32 28 31 bitrdi ⊢ x = a c → x = f ⁡ b g ⁡ d ↔ a = f ⁡ b ∧ c = g ⁡ d
33 32 2rexbidv ⊢ x = a c → ∃ b ∈ B ∃ d ∈ D x = f ⁡ b g ⁡ d ↔ ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
34 33 ralxp ⊢ ∀ x ∈ A × C ∃ b ∈ B ∃ d ∈ D x = f ⁡ b g ⁡ d ↔ ∀ a ∈ A ∀ c ∈ C ∃ b ∈ B ∃ d ∈ D a = f ⁡ b ∧ c = g ⁡ d
35 27 34 sylibr ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → ∀ x ∈ A × C ∃ b ∈ B ∃ d ∈ D x = f ⁡ b g ⁡ d
36 35 r19.21bi ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d ∧ x ∈ A × C → ∃ b ∈ B ∃ d ∈ D x = f ⁡ b g ⁡ d
37 vex ⊢ b ∈ V
38 vex ⊢ d ∈ V
39 37 38 op1std ⊢ y = b d → 1 st ⁡ y = b
40 39 fveq2d ⊢ y = b d → f ⁡ 1 st ⁡ y = f ⁡ b
41 37 38 op2ndd ⊢ y = b d → 2 nd ⁡ y = d
42 41 fveq2d ⊢ y = b d → g ⁡ 2 nd ⁡ y = g ⁡ d
43 40 42 opeq12d ⊢ y = b d → f ⁡ 1 st ⁡ y g ⁡ 2 nd ⁡ y = f ⁡ b g ⁡ d
44 43 eqeq2d ⊢ y = b d → x = f ⁡ 1 st ⁡ y g ⁡ 2 nd ⁡ y ↔ x = f ⁡ b g ⁡ d
45 44 rexxp ⊢ ∃ y ∈ B × D x = f ⁡ 1 st ⁡ y g ⁡ 2 nd ⁡ y ↔ ∃ b ∈ B ∃ d ∈ D x = f ⁡ b g ⁡ d
46 36 45 sylibr ⊢ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d ∧ x ∈ A × C → ∃ y ∈ B × D x = f ⁡ 1 st ⁡ y g ⁡ 2 nd ⁡ y
47 46 adantll ⊢ A ≼ * B ∧ C ≼ * D ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d ∧ x ∈ A × C → ∃ y ∈ B × D x = f ⁡ 1 st ⁡ y g ⁡ 2 nd ⁡ y
48 10 15 47 wdom2d ⊢ A ≼ * B ∧ C ≼ * D ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b ∧ ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → A × C ≼ * B × D
49 48 expr ⊢ A ≼ * B ∧ C ≼ * D ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → A × C ≼ * B × D
50 49 exlimdv ⊢ A ≼ * B ∧ C ≼ * D ∧ ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ g ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → A × C ≼ * B × D
51 50 ex ⊢ A ≼ * B ∧ C ≼ * D → ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ g ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → A × C ≼ * B × D
52 51 exlimdv ⊢ A ≼ * B ∧ C ≼ * D → ∃ f ∀ a ∈ A ∃ b ∈ B a = f ⁡ b → ∃ g ∀ c ∈ C ∃ d ∈ D c = g ⁡ d → A × C ≼ * B × D
53 2 4 52 mp2d ⊢ A ≼ * B ∧ C ≼ * D → A × C ≼ * B × D