Metamath Proof Explorer


Theorem dvdsmulf1o

Description: If M and N are two coprime integers, multiplication forms a bijection from the set of pairs <. j , k >. where j || M and k || N , to the set of divisors of M x. N . (Contributed by Mario Carneiro, 2-Jul-2015)

Ref Expression
Hypotheses dvdsmulf1o.1 ( 𝜑𝑀 ∈ ℕ )
dvdsmulf1o.2 ( 𝜑𝑁 ∈ ℕ )
dvdsmulf1o.3 ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
dvdsmulf1o.x 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥𝑀 }
dvdsmulf1o.y 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥𝑁 }
dvdsmulf1o.z 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
Assertion dvdsmulf1o ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto𝑍 )

Proof

Step Hyp Ref Expression
1 dvdsmulf1o.1 ( 𝜑𝑀 ∈ ℕ )
2 dvdsmulf1o.2 ( 𝜑𝑁 ∈ ℕ )
3 dvdsmulf1o.3 ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
4 dvdsmulf1o.x 𝑋 = { 𝑥 ∈ ℕ ∣ 𝑥𝑀 }
5 dvdsmulf1o.y 𝑌 = { 𝑥 ∈ ℕ ∣ 𝑥𝑁 }
6 dvdsmulf1o.z 𝑍 = { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑀 · 𝑁 ) }
7 ax-mulf · : ( ℂ × ℂ ) ⟶ ℂ
8 ffn ( · : ( ℂ × ℂ ) ⟶ ℂ → · Fn ( ℂ × ℂ ) )
9 7 8 ax-mp · Fn ( ℂ × ℂ )
10 4 ssrab3 𝑋 ⊆ ℕ
11 nnsscn ℕ ⊆ ℂ
12 10 11 sstri 𝑋 ⊆ ℂ
13 5 ssrab3 𝑌 ⊆ ℕ
14 13 11 sstri 𝑌 ⊆ ℂ
15 xpss12 ( ( 𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ ) → ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) )
16 12 14 15 mp2an ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ )
17 fnssres ( ( · Fn ( ℂ × ℂ ) ∧ ( 𝑋 × 𝑌 ) ⊆ ( ℂ × ℂ ) ) → ( · ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
18 9 16 17 mp2an ( · ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
19 18 a1i ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
20 ovres ( ( 𝑖𝑋𝑗𝑌 ) → ( 𝑖 ( · ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) = ( 𝑖 · 𝑗 ) )
21 20 adantl ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 ( · ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) = ( 𝑖 · 𝑗 ) )
22 breq1 ( 𝑥 = 𝑖 → ( 𝑥𝑀𝑖𝑀 ) )
23 22 4 elrab2 ( 𝑖𝑋 ↔ ( 𝑖 ∈ ℕ ∧ 𝑖𝑀 ) )
24 23 simplbi ( 𝑖𝑋𝑖 ∈ ℕ )
25 24 ad2antrl ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑖 ∈ ℕ )
26 breq1 ( 𝑥 = 𝑗 → ( 𝑥𝑁𝑗𝑁 ) )
27 26 5 elrab2 ( 𝑗𝑌 ↔ ( 𝑗 ∈ ℕ ∧ 𝑗𝑁 ) )
28 27 simplbi ( 𝑗𝑌𝑗 ∈ ℕ )
29 28 ad2antll ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑗 ∈ ℕ )
30 25 29 nnmulcld ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ ℕ )
31 27 simprbi ( 𝑗𝑌𝑗𝑁 )
32 31 ad2antll ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑗𝑁 )
33 23 simprbi ( 𝑖𝑋𝑖𝑀 )
34 33 ad2antrl ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑖𝑀 )
35 29 nnzd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑗 ∈ ℤ )
36 2 adantr ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑁 ∈ ℕ )
37 36 nnzd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑁 ∈ ℤ )
38 25 nnzd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑖 ∈ ℤ )
39 dvdscmul ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( 𝑗𝑁 → ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ) )
40 35 37 38 39 syl3anc ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑗𝑁 → ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ) )
41 1 adantr ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑀 ∈ ℕ )
42 41 nnzd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → 𝑀 ∈ ℤ )
43 dvdsmulc ( ( 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑖𝑀 → ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
44 38 42 37 43 syl3anc ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖𝑀 → ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) )
45 30 nnzd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ ℤ )
46 38 37 zmulcld ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 · 𝑁 ) ∈ ℤ )
47 42 37 zmulcld ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
48 dvdstr ( ( ( 𝑖 · 𝑗 ) ∈ ℤ ∧ ( 𝑖 · 𝑁 ) ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( ( ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ∧ ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
49 45 46 47 48 syl3anc ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( ( ( 𝑖 · 𝑗 ) ∥ ( 𝑖 · 𝑁 ) ∧ ( 𝑖 · 𝑁 ) ∥ ( 𝑀 · 𝑁 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
50 40 44 49 syl2and ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( ( 𝑗𝑁𝑖𝑀 ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
51 32 34 50 mp2and ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) )
52 breq1 ( 𝑥 = ( 𝑖 · 𝑗 ) → ( 𝑥 ∥ ( 𝑀 · 𝑁 ) ↔ ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
53 52 6 elrab2 ( ( 𝑖 · 𝑗 ) ∈ 𝑍 ↔ ( ( 𝑖 · 𝑗 ) ∈ ℕ ∧ ( 𝑖 · 𝑗 ) ∥ ( 𝑀 · 𝑁 ) ) )
54 30 51 53 sylanbrc ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 · 𝑗 ) ∈ 𝑍 )
55 21 54 eqeltrd ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ( 𝑖 ( · ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 )
56 55 ralrimivva ( 𝜑 → ∀ 𝑖𝑋𝑗𝑌 ( 𝑖 ( · ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 )
57 ffnov ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ↔ ( ( · ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ∀ 𝑖𝑋𝑗𝑌 ( 𝑖 ( · ↾ ( 𝑋 × 𝑌 ) ) 𝑗 ) ∈ 𝑍 ) )
58 19 56 57 sylanbrc ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 )
59 25 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℕ )
60 59 nnnn0d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℕ0 )
61 simprll ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚𝑋 )
62 breq1 ( 𝑥 = 𝑚 → ( 𝑥𝑀𝑚𝑀 ) )
63 62 4 elrab2 ( 𝑚𝑋 ↔ ( 𝑚 ∈ ℕ ∧ 𝑚𝑀 ) )
64 63 simplbi ( 𝑚𝑋𝑚 ∈ ℕ )
65 61 64 syl ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℕ )
66 65 nnnn0d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℕ0 )
67 59 nnzd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℤ )
68 29 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℕ )
69 68 nnzd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℤ )
70 dvdsmul1 ( ( 𝑖 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → 𝑖 ∥ ( 𝑖 · 𝑗 ) )
71 67 69 70 syl2anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ ( 𝑖 · 𝑗 ) )
72 simprr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) )
73 12 61 sselid ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℂ )
74 simprlr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛𝑌 )
75 breq1 ( 𝑥 = 𝑛 → ( 𝑥𝑁𝑛𝑁 ) )
76 75 5 elrab2 ( 𝑛𝑌 ↔ ( 𝑛 ∈ ℕ ∧ 𝑛𝑁 ) )
77 76 simplbi ( 𝑛𝑌𝑛 ∈ ℕ )
78 74 77 syl ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℕ )
79 78 nncnd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℂ )
80 73 79 mulcomd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 · 𝑛 ) = ( 𝑛 · 𝑚 ) )
81 72 80 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑛 · 𝑚 ) )
82 71 81 breqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∥ ( 𝑛 · 𝑚 ) )
83 78 nnzd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛 ∈ ℤ )
84 37 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑁 ∈ ℤ )
85 67 84 gcdcomd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑁 ) = ( 𝑁 gcd 𝑖 ) )
86 42 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑀 ∈ ℤ )
87 2 nnzd ( 𝜑𝑁 ∈ ℤ )
88 1 nnzd ( 𝜑𝑀 ∈ ℤ )
89 87 88 gcdcomd ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
90 89 3 eqtrd ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
91 90 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑀 ) = 1 )
92 34 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖𝑀 )
93 rpdvds ( ( ( 𝑁 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑁 gcd 𝑀 ) = 1 ∧ 𝑖𝑀 ) ) → ( 𝑁 gcd 𝑖 ) = 1 )
94 84 67 86 91 92 93 syl32anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑖 ) = 1 )
95 85 94 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑁 ) = 1 )
96 76 simprbi ( 𝑛𝑌𝑛𝑁 )
97 74 96 syl ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑛𝑁 )
98 rpdvds ( ( ( 𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑖 gcd 𝑁 ) = 1 ∧ 𝑛𝑁 ) ) → ( 𝑖 gcd 𝑛 ) = 1 )
99 67 83 84 95 97 98 syl32anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 gcd 𝑛 ) = 1 )
100 65 nnzd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∈ ℤ )
101 coprmdvds ( ( 𝑖 ∈ ℤ ∧ 𝑛 ∈ ℤ ∧ 𝑚 ∈ ℤ ) → ( ( 𝑖 ∥ ( 𝑛 · 𝑚 ) ∧ ( 𝑖 gcd 𝑛 ) = 1 ) → 𝑖𝑚 ) )
102 67 83 100 101 syl3anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( ( 𝑖 ∥ ( 𝑛 · 𝑚 ) ∧ ( 𝑖 gcd 𝑛 ) = 1 ) → 𝑖𝑚 ) )
103 82 99 102 mp2and ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖𝑚 )
104 dvdsmul1 ( ( 𝑚 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → 𝑚 ∥ ( 𝑚 · 𝑛 ) )
105 100 83 104 syl2anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ ( 𝑚 · 𝑛 ) )
106 59 nncnd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ∈ ℂ )
107 68 nncnd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 ∈ ℂ )
108 106 107 mulcomd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑗 · 𝑖 ) )
109 72 108 eqtr3d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 · 𝑛 ) = ( 𝑗 · 𝑖 ) )
110 105 109 breqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚 ∥ ( 𝑗 · 𝑖 ) )
111 100 84 gcdcomd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑁 ) = ( 𝑁 gcd 𝑚 ) )
112 63 simprbi ( 𝑚𝑋𝑚𝑀 )
113 61 112 syl ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚𝑀 )
114 rpdvds ( ( ( 𝑁 ∈ ℤ ∧ 𝑚 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( ( 𝑁 gcd 𝑀 ) = 1 ∧ 𝑚𝑀 ) ) → ( 𝑁 gcd 𝑚 ) = 1 )
115 84 100 86 91 113 114 syl32anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑁 gcd 𝑚 ) = 1 )
116 111 115 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑁 ) = 1 )
117 32 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗𝑁 )
118 rpdvds ( ( ( 𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( ( 𝑚 gcd 𝑁 ) = 1 ∧ 𝑗𝑁 ) ) → ( 𝑚 gcd 𝑗 ) = 1 )
119 100 69 84 116 117 118 syl32anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑚 gcd 𝑗 ) = 1 )
120 coprmdvds ( ( 𝑚 ∈ ℤ ∧ 𝑗 ∈ ℤ ∧ 𝑖 ∈ ℤ ) → ( ( 𝑚 ∥ ( 𝑗 · 𝑖 ) ∧ ( 𝑚 gcd 𝑗 ) = 1 ) → 𝑚𝑖 ) )
121 100 69 67 120 syl3anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( ( 𝑚 ∥ ( 𝑗 · 𝑖 ) ∧ ( 𝑚 gcd 𝑗 ) = 1 ) → 𝑚𝑖 ) )
122 110 119 121 mp2and ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑚𝑖 )
123 dvdseq ( ( ( 𝑖 ∈ ℕ0𝑚 ∈ ℕ0 ) ∧ ( 𝑖𝑚𝑚𝑖 ) ) → 𝑖 = 𝑚 )
124 60 66 103 122 123 syl22anc ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 = 𝑚 )
125 59 nnne0d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑖 ≠ 0 )
126 124 oveq1d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑛 ) = ( 𝑚 · 𝑛 ) )
127 72 126 eqtr4d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ( 𝑖 · 𝑗 ) = ( 𝑖 · 𝑛 ) )
128 107 79 106 125 127 mulcanad ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → 𝑗 = 𝑛 )
129 124 128 opeq12d ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( ( 𝑚𝑋𝑛𝑌 ) ∧ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ )
130 129 expr ( ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) ∧ ( 𝑚𝑋𝑛𝑌 ) ) → ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
131 130 ralrimivva ( ( 𝜑 ∧ ( 𝑖𝑋𝑗𝑌 ) ) → ∀ 𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
132 131 ralrimivva ( 𝜑 → ∀ 𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
133 fvres ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( · ‘ 𝑢 ) )
134 fvres ( 𝑣 ∈ ( 𝑋 × 𝑌 ) → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) = ( · ‘ 𝑣 ) )
135 133 134 eqeqan12d ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) ↔ ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) ) )
136 135 imbi1d ( ( 𝑢 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑣 ∈ ( 𝑋 × 𝑌 ) ) → ( ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
137 136 ralbidva ( 𝑢 ∈ ( 𝑋 × 𝑌 ) → ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
138 137 ralbiia ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
139 fveq2 ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( · ‘ 𝑣 ) = ( · ‘ ⟨ 𝑚 , 𝑛 ⟩ ) )
140 df-ov ( 𝑚 · 𝑛 ) = ( · ‘ ⟨ 𝑚 , 𝑛 ⟩ )
141 139 140 eqtr4di ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( · ‘ 𝑣 ) = ( 𝑚 · 𝑛 ) )
142 141 eqeq2d ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) ↔ ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) ) )
143 eqeq2 ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝑢 = 𝑣𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) )
144 142 143 imbi12d ( 𝑣 = ⟨ 𝑚 , 𝑛 ⟩ → ( ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ( ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
145 144 ralxp ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑚𝑋𝑛𝑌 ( ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) )
146 fveq2 ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( · ‘ 𝑢 ) = ( · ‘ ⟨ 𝑖 , 𝑗 ⟩ ) )
147 df-ov ( 𝑖 · 𝑗 ) = ( · ‘ ⟨ 𝑖 , 𝑗 ⟩ )
148 146 147 eqtr4di ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( · ‘ 𝑢 ) = ( 𝑖 · 𝑗 ) )
149 148 eqeq1d ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) ↔ ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) ) )
150 eqeq1 ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ↔ ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
151 149 150 imbi12d ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ↔ ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
152 151 2ralbidv ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ∀ 𝑚𝑋𝑛𝑌 ( ( · ‘ 𝑢 ) = ( 𝑚 · 𝑛 ) → 𝑢 = ⟨ 𝑚 , 𝑛 ⟩ ) ↔ ∀ 𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
153 145 152 syl5bb ( 𝑢 = ⟨ 𝑖 , 𝑗 ⟩ → ( ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) ) )
154 153 ralxp ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( · ‘ 𝑢 ) = ( · ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
155 138 154 bitri ( ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ↔ ∀ 𝑖𝑋𝑗𝑌𝑚𝑋𝑛𝑌 ( ( 𝑖 · 𝑗 ) = ( 𝑚 · 𝑛 ) → ⟨ 𝑖 , 𝑗 ⟩ = ⟨ 𝑚 , 𝑛 ⟩ ) )
156 132 155 sylibr ( 𝜑 → ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) )
157 dff13 ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1𝑍 ↔ ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑢 ∈ ( 𝑋 × 𝑌 ) ∀ 𝑣 ∈ ( 𝑋 × 𝑌 ) ( ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑣 ) → 𝑢 = 𝑣 ) ) )
158 58 156 157 sylanbrc ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1𝑍 )
159 breq1 ( 𝑥 = 𝑤 → ( 𝑥 ∥ ( 𝑀 · 𝑁 ) ↔ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
160 159 6 elrab2 ( 𝑤𝑍 ↔ ( 𝑤 ∈ ℕ ∧ 𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
161 160 simplbi ( 𝑤𝑍𝑤 ∈ ℕ )
162 161 adantl ( ( 𝜑𝑤𝑍 ) → 𝑤 ∈ ℕ )
163 162 nnzd ( ( 𝜑𝑤𝑍 ) → 𝑤 ∈ ℤ )
164 1 adantr ( ( 𝜑𝑤𝑍 ) → 𝑀 ∈ ℕ )
165 164 nnzd ( ( 𝜑𝑤𝑍 ) → 𝑀 ∈ ℤ )
166 164 nnne0d ( ( 𝜑𝑤𝑍 ) → 𝑀 ≠ 0 )
167 simpr ( ( 𝑤 = 0 ∧ 𝑀 = 0 ) → 𝑀 = 0 )
168 167 necon3ai ( 𝑀 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
169 166 168 syl ( ( 𝜑𝑤𝑍 ) → ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) )
170 gcdn0cl ( ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑀 = 0 ) ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
171 163 165 169 170 syl21anc ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑀 ) ∈ ℕ )
172 gcddvds ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
173 163 165 172 syl2anc ( ( 𝜑𝑤𝑍 ) → ( ( 𝑤 gcd 𝑀 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
174 173 simprd ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑀 ) ∥ 𝑀 )
175 breq1 ( 𝑥 = ( 𝑤 gcd 𝑀 ) → ( 𝑥𝑀 ↔ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
176 175 4 elrab2 ( ( 𝑤 gcd 𝑀 ) ∈ 𝑋 ↔ ( ( 𝑤 gcd 𝑀 ) ∈ ℕ ∧ ( 𝑤 gcd 𝑀 ) ∥ 𝑀 ) )
177 171 174 176 sylanbrc ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑀 ) ∈ 𝑋 )
178 2 adantr ( ( 𝜑𝑤𝑍 ) → 𝑁 ∈ ℕ )
179 178 nnzd ( ( 𝜑𝑤𝑍 ) → 𝑁 ∈ ℤ )
180 178 nnne0d ( ( 𝜑𝑤𝑍 ) → 𝑁 ≠ 0 )
181 simpr ( ( 𝑤 = 0 ∧ 𝑁 = 0 ) → 𝑁 = 0 )
182 181 necon3ai ( 𝑁 ≠ 0 → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
183 180 182 syl ( ( 𝜑𝑤𝑍 ) → ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) )
184 gcdn0cl ( ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑤 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
185 163 179 183 184 syl21anc ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑁 ) ∈ ℕ )
186 gcddvds ( ( 𝑤 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
187 163 179 186 syl2anc ( ( 𝜑𝑤𝑍 ) → ( ( 𝑤 gcd 𝑁 ) ∥ 𝑤 ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
188 187 simprd ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑁 ) ∥ 𝑁 )
189 breq1 ( 𝑥 = ( 𝑤 gcd 𝑁 ) → ( 𝑥𝑁 ↔ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
190 189 5 elrab2 ( ( 𝑤 gcd 𝑁 ) ∈ 𝑌 ↔ ( ( 𝑤 gcd 𝑁 ) ∈ ℕ ∧ ( 𝑤 gcd 𝑁 ) ∥ 𝑁 ) )
191 185 188 190 sylanbrc ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd 𝑁 ) ∈ 𝑌 )
192 177 191 opelxpd ( ( 𝜑𝑤𝑍 ) → ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
193 192 fvresd ( ( 𝜑𝑤𝑍 ) → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
194 3 adantr ( ( 𝜑𝑤𝑍 ) → ( 𝑀 gcd 𝑁 ) = 1 )
195 rpmulgcd2 ( ( ( 𝑤 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
196 163 165 179 194 195 syl31anc ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) )
197 df-ov ( ( 𝑤 gcd 𝑀 ) · ( 𝑤 gcd 𝑁 ) ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ )
198 196 197 eqtrdi ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = ( · ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
199 160 simprbi ( 𝑤𝑍𝑤 ∥ ( 𝑀 · 𝑁 ) )
200 199 adantl ( ( 𝜑𝑤𝑍 ) → 𝑤 ∥ ( 𝑀 · 𝑁 ) )
201 1 2 nnmulcld ( 𝜑 → ( 𝑀 · 𝑁 ) ∈ ℕ )
202 gcdeq ( ( 𝑤 ∈ ℕ ∧ ( 𝑀 · 𝑁 ) ∈ ℕ ) → ( ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
203 161 201 202 syl2anr ( ( 𝜑𝑤𝑍 ) → ( ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤𝑤 ∥ ( 𝑀 · 𝑁 ) ) )
204 200 203 mpbird ( ( 𝜑𝑤𝑍 ) → ( 𝑤 gcd ( 𝑀 · 𝑁 ) ) = 𝑤 )
205 193 198 204 3eqtr2rd ( ( 𝜑𝑤𝑍 ) → 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
206 fveq2 ( 𝑢 = ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ → ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) )
207 206 rspceeqv ( ( ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ∈ ( 𝑋 × 𝑌 ) ∧ 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝑤 gcd 𝑀 ) , ( 𝑤 gcd 𝑁 ) ⟩ ) ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
208 192 205 207 syl2anc ( ( 𝜑𝑤𝑍 ) → ∃ 𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
209 208 ralrimiva ( 𝜑 → ∀ 𝑤𝑍𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) )
210 dffo3 ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto𝑍 ↔ ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑍 ∧ ∀ 𝑤𝑍𝑢 ∈ ( 𝑋 × 𝑌 ) 𝑤 = ( ( · ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑢 ) ) )
211 58 209 210 sylanbrc ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto𝑍 )
212 df-f1o ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto𝑍 ↔ ( ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1𝑍 ∧ ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –onto𝑍 ) )
213 158 211 212 sylanbrc ( 𝜑 → ( · ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) –1-1-onto𝑍 )