Metamath Proof Explorer

Theorem mpodvdsmulf1o

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 . Version of dvdsmulf1o using maps-to notation, which does not require ax-mulf . (Contributed by GG, 18-Apr-2025)

Ref Expression
Hypotheses mpodvdsmulf1o.1 
|- ( ph -> M e. NN )
mpodvdsmulf1o.2 
|- ( ph -> N e. NN )
mpodvdsmulf1o.3 
|- ( ph -> ( M gcd N ) = 1 )
mpodvdsmulf1o.x 
|- X = { x e. NN | x || M }
mpodvdsmulf1o.y 
|- Y = { x e. NN | x || N }
mpodvdsmulf1o.z 
|- Z = { x e. NN | x || ( M x. N ) }
Assertion mpodvdsmulf1o 
|- ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )

Proof

Step Hyp Ref Expression
1 mpodvdsmulf1o.1 
 |-  ( ph -> M e. NN )
2 mpodvdsmulf1o.2 
 |-  ( ph -> N e. NN )
3 mpodvdsmulf1o.3 
 |-  ( ph -> ( M gcd N ) = 1 )
4 mpodvdsmulf1o.x 
 |-  X = { x e. NN | x || M }
5 mpodvdsmulf1o.y 
 |-  Y = { x e. NN | x || N }
6 mpodvdsmulf1o.z 
 |-  Z = { x e. NN | x || ( M x. N ) }
7 mpomulf 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
8 ffn 
 |-  ( ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC -> ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) )
9 7 8 ax-mp 
 |-  ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC )
10 4 ssrab3 
 |-  X C_ NN
11 nnsscn 
 |-  NN C_ CC
12 10 11 sstri 
 |-  X C_ CC
13 5 ssrab3 
 |-  Y C_ NN
14 13 11 sstri 
 |-  Y C_ CC
15 xpss12 
 |-  ( ( X C_ CC /\ Y C_ CC ) -> ( X X. Y ) C_ ( CC X. CC ) )
16 12 14 15 mp2an 
 |-  ( X X. Y ) C_ ( CC X. CC )
17 fnssres 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) Fn ( CC X. CC ) /\ ( X X. Y ) C_ ( CC X. CC ) ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) Fn ( X X. Y ) )
18 9 16 17 mp2an 
 |-  ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) Fn ( X X. Y )
19 18 a1i 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) Fn ( X X. Y ) )
20 ovres 
 |-  ( ( i e. X /\ j e. Y ) -> ( i ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) j ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
21 20 adantl 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) j ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
22 12 sseli 
 |-  ( i e. X -> i e. CC )
23 22 adantr 
 |-  ( ( i e. X /\ j e. Y ) -> i e. CC )
24 14 sseli 
 |-  ( j e. Y -> j e. CC )
25 24 adantl 
 |-  ( ( i e. X /\ j e. Y ) -> j e. CC )
26 ovmpot 
 |-  ( ( i e. CC /\ j e. CC ) -> ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( i x. j ) )
27 26 eqcomd 
 |-  ( ( i e. CC /\ j e. CC ) -> ( i x. j ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
28 23 25 27 syl2anc 
 |-  ( ( i e. X /\ j e. Y ) -> ( i x. j ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
29 28 adantl 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
30 10 sseli 
 |-  ( i e. X -> i e. NN )
31 30 ad2antrl 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i e. NN )
32 13 sseli 
 |-  ( j e. Y -> j e. NN )
33 32 ad2antll 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j e. NN )
34 31 33 nnmulcld 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. NN )
35 breq1 
 |-  ( x = j -> ( x || N <-> j || N ) )
36 35 5 elrab2 
 |-  ( j e. Y <-> ( j e. NN /\ j || N ) )
37 36 simprbi 
 |-  ( j e. Y -> j || N )
38 37 ad2antll 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j || N )
39 breq1 
 |-  ( x = i -> ( x || M <-> i || M ) )
40 39 4 elrab2 
 |-  ( i e. X <-> ( i e. NN /\ i || M ) )
41 40 simprbi 
 |-  ( i e. X -> i || M )
42 41 ad2antrl 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i || M )
43 33 nnzd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> j e. ZZ )
44 2 adantr 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> N e. NN )
45 44 nnzd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> N e. ZZ )
46 31 nnzd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> i e. ZZ )
47 dvdscmul 
 |-  ( ( j e. ZZ /\ N e. ZZ /\ i e. ZZ ) -> ( j || N -> ( i x. j ) || ( i x. N ) ) )
48 43 45 46 47 syl3anc 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( j || N -> ( i x. j ) || ( i x. N ) ) )
49 1 adantr 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> M e. NN )
50 49 nnzd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> M e. ZZ )
51 dvdsmulc 
 |-  ( ( i e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( i || M -> ( i x. N ) || ( M x. N ) ) )
52 46 50 45 51 syl3anc 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i || M -> ( i x. N ) || ( M x. N ) ) )
53 34 nnzd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. ZZ )
54 46 45 zmulcld 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. N ) e. ZZ )
55 50 45 zmulcld 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( M x. N ) e. ZZ )
56 dvdstr 
 |-  ( ( ( i x. j ) e. ZZ /\ ( i x. N ) e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( ( i x. j ) || ( i x. N ) /\ ( i x. N ) || ( M x. N ) ) -> ( i x. j ) || ( M x. N ) ) )
57 53 54 55 56 syl3anc 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( ( ( i x. j ) || ( i x. N ) /\ ( i x. N ) || ( M x. N ) ) -> ( i x. j ) || ( M x. N ) ) )
58 48 52 57 syl2and 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( ( j || N /\ i || M ) -> ( i x. j ) || ( M x. N ) ) )
59 38 42 58 mp2and 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) || ( M x. N ) )
60 breq1 
 |-  ( x = ( i x. j ) -> ( x || ( M x. N ) <-> ( i x. j ) || ( M x. N ) ) )
61 60 6 elrab2 
 |-  ( ( i x. j ) e. Z <-> ( ( i x. j ) e. NN /\ ( i x. j ) || ( M x. N ) ) )
62 34 59 61 sylanbrc 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i x. j ) e. Z )
63 29 62 eqeltrrd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) e. Z )
64 21 63 eqeltrd 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> ( i ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) j ) e. Z )
65 64 ralrimivva 
 |-  ( ph -> A. i e. X A. j e. Y ( i ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) j ) e. Z )
66 ffnov 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) --> Z <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) Fn ( X X. Y ) /\ A. i e. X A. j e. Y ( i ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) j ) e. Z ) )
67 19 65 66 sylanbrc 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) --> Z )
68 23 ad2antlr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> i e. CC )
69 25 ad2antlr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> j e. CC )
70 68 69 26 syl2anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( i x. j ) )
71 12 sseli 
 |-  ( m e. X -> m e. CC )
72 71 ad2antrl 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> m e. CC )
73 14 sseli 
 |-  ( n e. Y -> n e. CC )
74 73 ad2antll 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> n e. CC )
75 ovmpot 
 |-  ( ( m e. CC /\ n e. CC ) -> ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) = ( m x. n ) )
76 72 74 75 syl2anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) = ( m x. n ) )
77 70 76 eqeq12d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) <-> ( i x. j ) = ( m x. n ) ) )
78 31 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. NN )
79 78 nnnn0d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. NN0 )
80 simprll 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. X )
81 10 80 sselid 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. NN )
82 81 nnnn0d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. NN0 )
83 78 nnzd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. ZZ )
84 33 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. NN )
85 84 nnzd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. ZZ )
86 dvdsmul1 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> i || ( i x. j ) )
87 83 85 86 syl2anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || ( i x. j ) )
88 simprr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( m x. n ) )
89 12 80 sselid 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. CC )
90 simprlr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. Y )
91 14 90 sselid 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. CC )
92 89 91 mulcomd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m x. n ) = ( n x. m ) )
93 88 92 eqtrd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( n x. m ) )
94 87 93 breqtrd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || ( n x. m ) )
95 13 90 sselid 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. NN )
96 95 nnzd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n e. ZZ )
97 45 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> N e. ZZ )
98 83 97 gcdcomd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd N ) = ( N gcd i ) )
99 50 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> M e. ZZ )
100 2 nnzd 
 |-  ( ph -> N e. ZZ )
101 1 nnzd 
 |-  ( ph -> M e. ZZ )
102 100 101 gcdcomd 
 |-  ( ph -> ( N gcd M ) = ( M gcd N ) )
103 102 3 eqtrd 
 |-  ( ph -> ( N gcd M ) = 1 )
104 103 ad2antrr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd M ) = 1 )
105 42 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || M )
106 rpdvds 
 |-  ( ( ( N e. ZZ /\ i e. ZZ /\ M e. ZZ ) /\ ( ( N gcd M ) = 1 /\ i || M ) ) -> ( N gcd i ) = 1 )
107 97 83 99 104 105 106 syl32anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd i ) = 1 )
108 98 107 eqtrd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd N ) = 1 )
109 breq1 
 |-  ( x = n -> ( x || N <-> n || N ) )
110 109 5 elrab2 
 |-  ( n e. Y <-> ( n e. NN /\ n || N ) )
111 110 simprbi 
 |-  ( n e. Y -> n || N )
112 90 111 syl 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> n || N )
113 rpdvds 
 |-  ( ( ( i e. ZZ /\ n e. ZZ /\ N e. ZZ ) /\ ( ( i gcd N ) = 1 /\ n || N ) ) -> ( i gcd n ) = 1 )
114 83 96 97 108 112 113 syl32anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i gcd n ) = 1 )
115 81 nnzd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m e. ZZ )
116 coprmdvds 
 |-  ( ( i e. ZZ /\ n e. ZZ /\ m e. ZZ ) -> ( ( i || ( n x. m ) /\ ( i gcd n ) = 1 ) -> i || m ) )
117 83 96 115 116 syl3anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( ( i || ( n x. m ) /\ ( i gcd n ) = 1 ) -> i || m ) )
118 94 114 117 mp2and 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i || m )
119 dvdsmul1 
 |-  ( ( m e. ZZ /\ n e. ZZ ) -> m || ( m x. n ) )
120 115 96 119 syl2anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || ( m x. n ) )
121 78 nncnd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i e. CC )
122 84 nncnd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j e. CC )
123 121 122 mulcomd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( j x. i ) )
124 88 123 eqtr3d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m x. n ) = ( j x. i ) )
125 120 124 breqtrd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || ( j x. i ) )
126 115 97 gcdcomd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd N ) = ( N gcd m ) )
127 breq1 
 |-  ( x = m -> ( x || M <-> m || M ) )
128 127 4 elrab2 
 |-  ( m e. X <-> ( m e. NN /\ m || M ) )
129 128 simprbi 
 |-  ( m e. X -> m || M )
130 80 129 syl 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || M )
131 rpdvds 
 |-  ( ( ( N e. ZZ /\ m e. ZZ /\ M e. ZZ ) /\ ( ( N gcd M ) = 1 /\ m || M ) ) -> ( N gcd m ) = 1 )
132 97 115 99 104 130 131 syl32anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( N gcd m ) = 1 )
133 126 132 eqtrd 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd N ) = 1 )
134 38 adantr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j || N )
135 rpdvds 
 |-  ( ( ( m e. ZZ /\ j e. ZZ /\ N e. ZZ ) /\ ( ( m gcd N ) = 1 /\ j || N ) ) -> ( m gcd j ) = 1 )
136 115 85 97 133 134 135 syl32anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( m gcd j ) = 1 )
137 coprmdvds 
 |-  ( ( m e. ZZ /\ j e. ZZ /\ i e. ZZ ) -> ( ( m || ( j x. i ) /\ ( m gcd j ) = 1 ) -> m || i ) )
138 115 85 83 137 syl3anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( ( m || ( j x. i ) /\ ( m gcd j ) = 1 ) -> m || i ) )
139 125 136 138 mp2and 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> m || i )
140 dvdseq 
 |-  ( ( ( i e. NN0 /\ m e. NN0 ) /\ ( i || m /\ m || i ) ) -> i = m )
141 79 82 118 139 140 syl22anc 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i = m )
142 78 nnne0d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> i =/= 0 )
143 141 oveq1d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. n ) = ( m x. n ) )
144 88 143 eqtr4d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> ( i x. j ) = ( i x. n ) )
145 122 91 121 142 144 mulcanad 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> j = n )
146 141 145 opeq12d 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( ( m e. X /\ n e. Y ) /\ ( i x. j ) = ( m x. n ) ) ) -> <. i , j >. = <. m , n >. )
147 146 expr 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( ( i x. j ) = ( m x. n ) -> <. i , j >. = <. m , n >. ) )
148 77 147 sylbid 
 |-  ( ( ( ph /\ ( i e. X /\ j e. Y ) ) /\ ( m e. X /\ n e. Y ) ) -> ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) )
149 148 ralrimivva 
 |-  ( ( ph /\ ( i e. X /\ j e. Y ) ) -> A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) )
150 149 ralrimivva 
 |-  ( ph -> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) )
151 fvres 
 |-  ( u e. ( X X. Y ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) )
152 fvres 
 |-  ( v e. ( X X. Y ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) )
153 151 152 eqeqan12d 
 |-  ( ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) -> ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) ) )
154 153 imbi1d 
 |-  ( ( u e. ( X X. Y ) /\ v e. ( X X. Y ) ) -> ( ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) ) )
155 154 ralbidva 
 |-  ( u e. ( X X. Y ) -> ( A. v e. ( X X. Y ) ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. v e. ( X X. Y ) ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) ) )
156 155 ralbiia 
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) )
157 fveq2 
 |-  ( v = <. m , n >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. m , n >. ) )
158 df-ov 
 |-  ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. m , n >. )
159 157 158 eqtr4di 
 |-  ( v = <. m , n >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) )
160 159 eqeq2d 
 |-  ( v = <. m , n >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) <-> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) ) )
161 eqeq2 
 |-  ( v = <. m , n >. -> ( u = v <-> u = <. m , n >. ) )
162 160 161 imbi12d 
 |-  ( v = <. m , n >. -> ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> u = <. m , n >. ) ) )
163 162 ralxp 
 |-  ( A. v e. ( X X. Y ) ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) <-> A. m e. X A. n e. Y ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> u = <. m , n >. ) )
164 fveq2 
 |-  ( u = <. i , j >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. i , j >. ) )
165 df-ov 
 |-  ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. i , j >. )
166 164 165 eqtr4di 
 |-  ( u = <. i , j >. -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) )
167 166 eqeq1d 
 |-  ( u = <. i , j >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) <-> ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) ) )
168 eqeq1 
 |-  ( u = <. i , j >. -> ( u = <. m , n >. <-> <. i , j >. = <. m , n >. ) )
169 167 168 imbi12d 
 |-  ( u = <. i , j >. -> ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> u = <. m , n >. ) <-> ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) ) )
170 169 2ralbidv 
 |-  ( u = <. i , j >. -> ( A. m e. X A. n e. Y ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> u = <. m , n >. ) <-> A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) ) )
171 163 170 bitrid 
 |-  ( u = <. i , j >. -> ( A. v e. ( X X. Y ) ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) <-> A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) ) )
172 171 ralxp 
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` u ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` v ) -> u = v ) <-> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) )
173 156 172 bitri 
 |-  ( A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) <-> A. i e. X A. j e. Y A. m e. X A. n e. Y ( ( i ( x e. CC , y e. CC |-> ( x x. y ) ) j ) = ( m ( x e. CC , y e. CC |-> ( x x. y ) ) n ) -> <. i , j >. = <. m , n >. ) )
174 150 173 sylibr 
 |-  ( ph -> A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) )
175 dff13 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) --> Z /\ A. u e. ( X X. Y ) A. v e. ( X X. Y ) ( ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` v ) -> u = v ) ) )
176 67 174 175 sylanbrc 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z )
177 breq1 
 |-  ( x = w -> ( x || ( M x. N ) <-> w || ( M x. N ) ) )
178 177 6 elrab2 
 |-  ( w e. Z <-> ( w e. NN /\ w || ( M x. N ) ) )
179 178 simplbi 
 |-  ( w e. Z -> w e. NN )
180 179 adantl 
 |-  ( ( ph /\ w e. Z ) -> w e. NN )
181 180 nnzd 
 |-  ( ( ph /\ w e. Z ) -> w e. ZZ )
182 1 adantr 
 |-  ( ( ph /\ w e. Z ) -> M e. NN )
183 182 nnzd 
 |-  ( ( ph /\ w e. Z ) -> M e. ZZ )
184 182 nnne0d 
 |-  ( ( ph /\ w e. Z ) -> M =/= 0 )
185 simpr 
 |-  ( ( w = 0 /\ M = 0 ) -> M = 0 )
186 185 necon3ai 
 |-  ( M =/= 0 -> -. ( w = 0 /\ M = 0 ) )
187 184 186 syl 
 |-  ( ( ph /\ w e. Z ) -> -. ( w = 0 /\ M = 0 ) )
188 gcdn0cl 
 |-  ( ( ( w e. ZZ /\ M e. ZZ ) /\ -. ( w = 0 /\ M = 0 ) ) -> ( w gcd M ) e. NN )
189 181 183 187 188 syl21anc 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) e. NN )
190 gcddvds 
 |-  ( ( w e. ZZ /\ M e. ZZ ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
191 181 183 190 syl2anc 
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd M ) || w /\ ( w gcd M ) || M ) )
192 191 simprd 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) || M )
193 breq1 
 |-  ( x = ( w gcd M ) -> ( x || M <-> ( w gcd M ) || M ) )
194 193 4 elrab2 
 |-  ( ( w gcd M ) e. X <-> ( ( w gcd M ) e. NN /\ ( w gcd M ) || M ) )
195 189 192 194 sylanbrc 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) e. X )
196 2 adantr 
 |-  ( ( ph /\ w e. Z ) -> N e. NN )
197 196 nnzd 
 |-  ( ( ph /\ w e. Z ) -> N e. ZZ )
198 196 nnne0d 
 |-  ( ( ph /\ w e. Z ) -> N =/= 0 )
199 simpr 
 |-  ( ( w = 0 /\ N = 0 ) -> N = 0 )
200 199 necon3ai 
 |-  ( N =/= 0 -> -. ( w = 0 /\ N = 0 ) )
201 198 200 syl 
 |-  ( ( ph /\ w e. Z ) -> -. ( w = 0 /\ N = 0 ) )
202 gcdn0cl 
 |-  ( ( ( w e. ZZ /\ N e. ZZ ) /\ -. ( w = 0 /\ N = 0 ) ) -> ( w gcd N ) e. NN )
203 181 197 201 202 syl21anc 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) e. NN )
204 gcddvds 
 |-  ( ( w e. ZZ /\ N e. ZZ ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
205 181 197 204 syl2anc 
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd N ) || w /\ ( w gcd N ) || N ) )
206 205 simprd 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) || N )
207 breq1 
 |-  ( x = ( w gcd N ) -> ( x || N <-> ( w gcd N ) || N ) )
208 207 5 elrab2 
 |-  ( ( w gcd N ) e. Y <-> ( ( w gcd N ) e. NN /\ ( w gcd N ) || N ) )
209 203 206 208 sylanbrc 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) e. Y )
210 195 209 opelxpd 
 |-  ( ( ph /\ w e. Z ) -> <. ( w gcd M ) , ( w gcd N ) >. e. ( X X. Y ) )
211 210 fvresd 
 |-  ( ( ph /\ w e. Z ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) )
212 df-ov 
 |-  ( ( w gcd M ) ( x e. CC , y e. CC |-> ( x x. y ) ) ( w gcd N ) ) = ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. )
213 189 nncnd 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd M ) e. CC )
214 203 nncnd 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd N ) e. CC )
215 ovmpot 
 |-  ( ( ( w gcd M ) e. CC /\ ( w gcd N ) e. CC ) -> ( ( w gcd M ) ( x e. CC , y e. CC |-> ( x x. y ) ) ( w gcd N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
216 213 214 215 syl2anc 
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd M ) ( x e. CC , y e. CC |-> ( x x. y ) ) ( w gcd N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
217 212 216 eqtr3id 
 |-  ( ( ph /\ w e. Z ) -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) = ( ( w gcd M ) x. ( w gcd N ) ) )
218 df-ov 
 |-  ( ( w gcd M ) x. ( w gcd N ) ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. )
219 218 a1i 
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd M ) x. ( w gcd N ) ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. ) )
220 211 217 219 3eqtrd 
 |-  ( ( ph /\ w e. Z ) -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. ) )
221 3 adantr 
 |-  ( ( ph /\ w e. Z ) -> ( M gcd N ) = 1 )
222 rpmulgcd2 
 |-  ( ( ( w e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ ( M gcd N ) = 1 ) -> ( w gcd ( M x. N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
223 181 183 197 221 222 syl31anc 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = ( ( w gcd M ) x. ( w gcd N ) ) )
224 223 218 eqtrdi 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = ( x. ` <. ( w gcd M ) , ( w gcd N ) >. ) )
225 178 simprbi 
 |-  ( w e. Z -> w || ( M x. N ) )
226 225 adantl 
 |-  ( ( ph /\ w e. Z ) -> w || ( M x. N ) )
227 1 2 nnmulcld 
 |-  ( ph -> ( M x. N ) e. NN )
228 gcdeq 
 |-  ( ( w e. NN /\ ( M x. N ) e. NN ) -> ( ( w gcd ( M x. N ) ) = w <-> w || ( M x. N ) ) )
229 179 227 228 syl2anr 
 |-  ( ( ph /\ w e. Z ) -> ( ( w gcd ( M x. N ) ) = w <-> w || ( M x. N ) ) )
230 226 229 mpbird 
 |-  ( ( ph /\ w e. Z ) -> ( w gcd ( M x. N ) ) = w )
231 220 224 230 3eqtr2rd 
 |-  ( ( ph /\ w e. Z ) -> w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) )
232 fveq2 
 |-  ( u = <. ( w gcd M ) , ( w gcd N ) >. -> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) )
233 232 rspceeqv 
 |-  ( ( <. ( w gcd M ) , ( w gcd N ) >. e. ( X X. Y ) /\ w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` <. ( w gcd M ) , ( w gcd N ) >. ) ) -> E. u e. ( X X. Y ) w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) )
234 210 231 233 syl2anc 
 |-  ( ( ph /\ w e. Z ) -> E. u e. ( X X. Y ) w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) )
235 234 ralrimiva 
 |-  ( ph -> A. w e. Z E. u e. ( X X. Y ) w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) )
236 dffo3 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) --> Z /\ A. w e. Z E. u e. ( X X. Y ) w = ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) ` u ) ) )
237 67 235 236 sylanbrc 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z )
238 df-f1o 
 |-  ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z <-> ( ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-> Z /\ ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -onto-> Z ) )
239 176 237 238 sylanbrc 
 |-  ( ph -> ( ( x e. CC , y e. CC |-> ( x x. y ) ) |` ( X X. Y ) ) : ( X X. Y ) -1-1-onto-> Z )