This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ ∪ 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 bitrid ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑓 : 𝐴 –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 ⊢ ( 𝐴 ≼ 𝐵 → ( 𝐶 × 𝐴 ) ≼ ( 𝐶 × 𝐵 ) )