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 ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 brwdom3i ⊢ ( 𝐴 ≼* 𝐵 → ∃ 𝑓 ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) )
2 1 adantr ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ∃ 𝑓 ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) )
3 brwdom3i ⊢ ( 𝐶 ≼* 𝐷 → ∃ 𝑔 ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) )
4 3 adantl ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ∃ 𝑔 ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) )
5 relwdom ⊢ Rel ≼*
6 5 brrelex1i ⊢ ( 𝐴 ≼* 𝐵 → 𝐴 ∈ V )
7 5 brrelex1i ⊢ ( 𝐶 ≼* 𝐷 → 𝐶 ∈ V )
8 xpexg ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 × 𝐶 ) ∈ V )
9 6 7 8 syl2an ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( 𝐴 × 𝐶 ) ∈ V )
10 9 adantr ⊢ ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) → ( 𝐴 × 𝐶 ) ∈ V )
11 5 brrelex2i ⊢ ( 𝐴 ≼* 𝐵 → 𝐵 ∈ V )
12 5 brrelex2i ⊢ ( 𝐶 ≼* 𝐷 → 𝐷 ∈ V )
13 xpexg ⊢ ( ( 𝐵 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐵 × 𝐷 ) ∈ V )
14 11 12 13 syl2an ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( 𝐵 × 𝐷 ) ∈ V )
15 14 adantr ⊢ ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) → ( 𝐵 × 𝐷 ) ∈ V )
16 pm3.2 ⊢ ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
17 16 ralimdv ⊢ ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ∀ 𝑐 ∈ 𝐶 ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
18 17 com12 ⊢ ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ∀ 𝑐 ∈ 𝐶 ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
19 18 ralimdv ⊢ ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
20 19 impcom ⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
21 pm3.2 ⊢ ( 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
22 21 reximdv ⊢ ( 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
23 22 com12 ⊢ ( ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝑎 = ( 𝑓 ‘ 𝑏 ) → ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
24 23 reximdv ⊢ ( ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
25 24 impcom ⊢ ( ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
26 25 2ralimi ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ( ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
27 20 26 syl ⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
28 eqeq1 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑐 ⟩ → ( 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ↔ ⟨ 𝑎 , 𝑐 ⟩ = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ) )
29 vex ⊢ 𝑎 ∈ V
30 vex ⊢ 𝑐 ∈ V
31 29 30 opth ⊢ ( ⟨ 𝑎 , 𝑐 ⟩ = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ↔ ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
32 28 31 syl6bb ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑐 ⟩ → ( 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ↔ ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
33 32 2rexbidv ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑐 ⟩ → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) )
34 33 ralxp ⊢ ( ∀ 𝑥 ∈ ( 𝐴 × 𝐶 ) ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑐 ∈ 𝐶 ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 ( 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ 𝑐 = ( 𝑔 ‘ 𝑑 ) ) )
35 27 34 sylibr ⊢ ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) → ∀ 𝑥 ∈ ( 𝐴 × 𝐶 ) ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ )
36 35 r19.21bi ⊢ ( ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ∧ 𝑥 ∈ ( 𝐴 × 𝐶 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ )
37 vex ⊢ 𝑏 ∈ V
38 vex ⊢ 𝑑 ∈ V
39 37 38 op1std ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ( 1st ‘ 𝑦 ) = 𝑏 )
40 39 fveq2d ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) = ( 𝑓 ‘ 𝑏 ) )
41 37 38 op2ndd ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ( 2nd ‘ 𝑦 ) = 𝑑 )
42 41 fveq2d ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) = ( 𝑔 ‘ 𝑑 ) )
43 40 42 opeq12d ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ⟨ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ⟩ = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ )
44 43 eqeq2d ⊢ ( 𝑦 = ⟨ 𝑏 , 𝑑 ⟩ → ( 𝑥 = ⟨ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ↔ 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ ) )
45 44 rexxp ⊢ ( ∃ 𝑦 ∈ ( 𝐵 × 𝐷 ) 𝑥 = ⟨ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ⟩ ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑑 ∈ 𝐷 𝑥 = ⟨ ( 𝑓 ‘ 𝑏 ) , ( 𝑔 ‘ 𝑑 ) ⟩ )
46 36 45 sylibr ⊢ ( ( ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ∧ 𝑥 ∈ ( 𝐴 × 𝐶 ) ) → ∃ 𝑦 ∈ ( 𝐵 × 𝐷 ) 𝑥 = ⟨ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ⟩ )
47 46 adantll ⊢ ( ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) ∧ 𝑥 ∈ ( 𝐴 × 𝐶 ) ) → ∃ 𝑦 ∈ ( 𝐵 × 𝐷 ) 𝑥 = ⟨ ( 𝑓 ‘ ( 1st ‘ 𝑦 ) ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ⟩ )
48 10 15 47 wdom2d ⊢ ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) ) ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) )
49 48 expr ⊢ ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ) → ( ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) ) )
50 49 exlimdv ⊢ ( ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) ∧ ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) ) → ( ∃ 𝑔 ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) ) )
51 50 ex ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( ∃ 𝑔 ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) ) ) )
52 51 exlimdv ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( ∃ 𝑓 ∀ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝑓 ‘ 𝑏 ) → ( ∃ 𝑔 ∀ 𝑐 ∈ 𝐶 ∃ 𝑑 ∈ 𝐷 𝑐 = ( 𝑔 ‘ 𝑑 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) ) ) )
53 2 4 52 mp2d ⊢ ( ( 𝐴 ≼* 𝐵 ∧ 𝐶 ≼* 𝐷 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) )