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 𝐶 ∈ V
Assertion xpdom2 ( 𝐴𝐵 → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) )

Proof

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