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 bitrdi ( 𝑥 = ⟨ 𝑎 , 𝑐 ⟩ → ( 𝑥 = ⟨ ( 𝑓𝑏 ) , ( 𝑔𝑑 ) ⟩ ↔ ( 𝑎 = ( 𝑓𝑏 ) ∧ 𝑐 = ( 𝑔𝑑 ) ) ) )
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 ( ( 𝐴* 𝐵𝐶* 𝐷 ) → ( 𝐴 × 𝐶 ) ≼* ( 𝐵 × 𝐷 ) )