Metamath Proof Explorer

Theorem f1od2

Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by Thierry Arnoux, 17-Aug-2017)

Ref Expression
Hypotheses f1od2.1 
|- F = ( x e. A , y e. B |-> C )
f1od2.2 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. W )
f1od2.3 
|- ( ( ph /\ z e. D ) -> ( I e. X /\ J e. Y ) )
f1od2.4 
|- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( z e. D /\ ( x = I /\ y = J ) ) ) )
Assertion f1od2 
|- ( ph -> F : ( A X. B ) -1-1-onto-> D )

Proof

Step Hyp Ref Expression
1 f1od2.1 
 |-  F = ( x e. A , y e. B |-> C )
2 f1od2.2 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. W )
3 f1od2.3 
 |-  ( ( ph /\ z e. D ) -> ( I e. X /\ J e. Y ) )
4 f1od2.4 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( z e. D /\ ( x = I /\ y = J ) ) ) )
5 2 ralrimivva 
 |-  ( ph -> A. x e. A A. y e. B C e. W )
6 1 fnmpo 
 |-  ( A. x e. A A. y e. B C e. W -> F Fn ( A X. B ) )
7 5 6 syl 
 |-  ( ph -> F Fn ( A X. B ) )
8 opelxpi 
 |-  ( ( I e. X /\ J e. Y ) -> <. I , J >. e. ( X X. Y ) )
9 3 8 syl 
 |-  ( ( ph /\ z e. D ) -> <. I , J >. e. ( X X. Y ) )
10 9 ralrimiva 
 |-  ( ph -> A. z e. D <. I , J >. e. ( X X. Y ) )
11 eqid 
 |-  ( z e. D |-> <. I , J >. ) = ( z e. D |-> <. I , J >. )
12 11 fnmpt 
 |-  ( A. z e. D <. I , J >. e. ( X X. Y ) -> ( z e. D |-> <. I , J >. ) Fn D )
13 10 12 syl 
 |-  ( ph -> ( z e. D |-> <. I , J >. ) Fn D )
14 elxp7 
 |-  ( a e. ( A X. B ) <-> ( a e. ( _V X. _V ) /\ ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) ) )
15 14 anbi1i 
 |-  ( ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( ( a e. ( _V X. _V ) /\ ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) )
16 anass 
 |-  ( ( ( a e. ( _V X. _V ) /\ ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( a e. ( _V X. _V ) /\ ( ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) ) )
17 4 sbcbidv 
 |-  ( ph -> ( [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) ) )
18 17 sbcbidv 
 |-  ( ph -> ( [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) ) )
19 sbcan 
 |-  ( [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( [. ( 2nd ` a ) / y ]. ( x e. A /\ y e. B ) /\ [. ( 2nd ` a ) / y ]. z = C ) )
20 sbcan 
 |-  ( [. ( 2nd ` a ) / y ]. ( x e. A /\ y e. B ) <-> ( [. ( 2nd ` a ) / y ]. x e. A /\ [. ( 2nd ` a ) / y ]. y e. B ) )
21 fvex 
 |-  ( 2nd ` a ) e. _V
22 sbcg 
 |-  ( ( 2nd ` a ) e. _V -> ( [. ( 2nd ` a ) / y ]. x e. A <-> x e. A ) )
23 21 22 ax-mp 
 |-  ( [. ( 2nd ` a ) / y ]. x e. A <-> x e. A )
24 sbcel1v 
 |-  ( [. ( 2nd ` a ) / y ]. y e. B <-> ( 2nd ` a ) e. B )
25 23 24 anbi12i 
 |-  ( ( [. ( 2nd ` a ) / y ]. x e. A /\ [. ( 2nd ` a ) / y ]. y e. B ) <-> ( x e. A /\ ( 2nd ` a ) e. B ) )
26 20 25 bitri 
 |-  ( [. ( 2nd ` a ) / y ]. ( x e. A /\ y e. B ) <-> ( x e. A /\ ( 2nd ` a ) e. B ) )
27 sbceq2g 
 |-  ( ( 2nd ` a ) e. _V -> ( [. ( 2nd ` a ) / y ]. z = C <-> z = [_ ( 2nd ` a ) / y ]_ C ) )
28 21 27 ax-mp 
 |-  ( [. ( 2nd ` a ) / y ]. z = C <-> z = [_ ( 2nd ` a ) / y ]_ C )
29 26 28 anbi12i 
 |-  ( ( [. ( 2nd ` a ) / y ]. ( x e. A /\ y e. B ) /\ [. ( 2nd ` a ) / y ]. z = C ) <-> ( ( x e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 2nd ` a ) / y ]_ C ) )
30 19 29 bitri 
 |-  ( [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 2nd ` a ) / y ]_ C ) )
31 30 sbcbii 
 |-  ( [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> [. ( 1st ` a ) / x ]. ( ( x e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 2nd ` a ) / y ]_ C ) )
32 sbcan 
 |-  ( [. ( 1st ` a ) / x ]. ( ( x e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 2nd ` a ) / y ]_ C ) <-> ( [. ( 1st ` a ) / x ]. ( x e. A /\ ( 2nd ` a ) e. B ) /\ [. ( 1st ` a ) / x ]. z = [_ ( 2nd ` a ) / y ]_ C ) )
33 sbcan 
 |-  ( [. ( 1st ` a ) / x ]. ( x e. A /\ ( 2nd ` a ) e. B ) <-> ( [. ( 1st ` a ) / x ]. x e. A /\ [. ( 1st ` a ) / x ]. ( 2nd ` a ) e. B ) )
34 sbcel1v 
 |-  ( [. ( 1st ` a ) / x ]. x e. A <-> ( 1st ` a ) e. A )
35 fvex 
 |-  ( 1st ` a ) e. _V
36 sbcg 
 |-  ( ( 1st ` a ) e. _V -> ( [. ( 1st ` a ) / x ]. ( 2nd ` a ) e. B <-> ( 2nd ` a ) e. B ) )
37 35 36 ax-mp 
 |-  ( [. ( 1st ` a ) / x ]. ( 2nd ` a ) e. B <-> ( 2nd ` a ) e. B )
38 34 37 anbi12i 
 |-  ( ( [. ( 1st ` a ) / x ]. x e. A /\ [. ( 1st ` a ) / x ]. ( 2nd ` a ) e. B ) <-> ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) )
39 33 38 bitri 
 |-  ( [. ( 1st ` a ) / x ]. ( x e. A /\ ( 2nd ` a ) e. B ) <-> ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) )
40 sbceq2g 
 |-  ( ( 1st ` a ) e. _V -> ( [. ( 1st ` a ) / x ]. z = [_ ( 2nd ` a ) / y ]_ C <-> z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) )
41 35 40 ax-mp 
 |-  ( [. ( 1st ` a ) / x ]. z = [_ ( 2nd ` a ) / y ]_ C <-> z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C )
42 39 41 anbi12i 
 |-  ( ( [. ( 1st ` a ) / x ]. ( x e. A /\ ( 2nd ` a ) e. B ) /\ [. ( 1st ` a ) / x ]. z = [_ ( 2nd ` a ) / y ]_ C ) <-> ( ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) )
43 31 32 42 3bitri 
 |-  ( [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) )
44 sbcan 
 |-  ( [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) <-> ( [. ( 2nd ` a ) / y ]. z e. D /\ [. ( 2nd ` a ) / y ]. ( x = I /\ y = J ) ) )
45 sbcg 
 |-  ( ( 2nd ` a ) e. _V -> ( [. ( 2nd ` a ) / y ]. z e. D <-> z e. D ) )
46 21 45 ax-mp 
 |-  ( [. ( 2nd ` a ) / y ]. z e. D <-> z e. D )
47 sbcan 
 |-  ( [. ( 2nd ` a ) / y ]. ( x = I /\ y = J ) <-> ( [. ( 2nd ` a ) / y ]. x = I /\ [. ( 2nd ` a ) / y ]. y = J ) )
48 sbcg 
 |-  ( ( 2nd ` a ) e. _V -> ( [. ( 2nd ` a ) / y ]. x = I <-> x = I ) )
49 21 48 ax-mp 
 |-  ( [. ( 2nd ` a ) / y ]. x = I <-> x = I )
50 sbceq1g 
 |-  ( ( 2nd ` a ) e. _V -> ( [. ( 2nd ` a ) / y ]. y = J <-> [_ ( 2nd ` a ) / y ]_ y = J ) )
51 21 50 ax-mp 
 |-  ( [. ( 2nd ` a ) / y ]. y = J <-> [_ ( 2nd ` a ) / y ]_ y = J )
52 21 csbvargi 
 |-  [_ ( 2nd ` a ) / y ]_ y = ( 2nd ` a )
53 52 eqeq1i 
 |-  ( [_ ( 2nd ` a ) / y ]_ y = J <-> ( 2nd ` a ) = J )
54 51 53 bitri 
 |-  ( [. ( 2nd ` a ) / y ]. y = J <-> ( 2nd ` a ) = J )
55 49 54 anbi12i 
 |-  ( ( [. ( 2nd ` a ) / y ]. x = I /\ [. ( 2nd ` a ) / y ]. y = J ) <-> ( x = I /\ ( 2nd ` a ) = J ) )
56 47 55 bitri 
 |-  ( [. ( 2nd ` a ) / y ]. ( x = I /\ y = J ) <-> ( x = I /\ ( 2nd ` a ) = J ) )
57 46 56 anbi12i 
 |-  ( ( [. ( 2nd ` a ) / y ]. z e. D /\ [. ( 2nd ` a ) / y ]. ( x = I /\ y = J ) ) <-> ( z e. D /\ ( x = I /\ ( 2nd ` a ) = J ) ) )
58 44 57 bitri 
 |-  ( [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) <-> ( z e. D /\ ( x = I /\ ( 2nd ` a ) = J ) ) )
59 58 sbcbii 
 |-  ( [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) <-> [. ( 1st ` a ) / x ]. ( z e. D /\ ( x = I /\ ( 2nd ` a ) = J ) ) )
60 sbcan 
 |-  ( [. ( 1st ` a ) / x ]. ( z e. D /\ ( x = I /\ ( 2nd ` a ) = J ) ) <-> ( [. ( 1st ` a ) / x ]. z e. D /\ [. ( 1st ` a ) / x ]. ( x = I /\ ( 2nd ` a ) = J ) ) )
61 sbcg 
 |-  ( ( 1st ` a ) e. _V -> ( [. ( 1st ` a ) / x ]. z e. D <-> z e. D ) )
62 35 61 ax-mp 
 |-  ( [. ( 1st ` a ) / x ]. z e. D <-> z e. D )
63 sbcan 
 |-  ( [. ( 1st ` a ) / x ]. ( x = I /\ ( 2nd ` a ) = J ) <-> ( [. ( 1st ` a ) / x ]. x = I /\ [. ( 1st ` a ) / x ]. ( 2nd ` a ) = J ) )
64 sbceq1g 
 |-  ( ( 1st ` a ) e. _V -> ( [. ( 1st ` a ) / x ]. x = I <-> [_ ( 1st ` a ) / x ]_ x = I ) )
65 35 64 ax-mp 
 |-  ( [. ( 1st ` a ) / x ]. x = I <-> [_ ( 1st ` a ) / x ]_ x = I )
66 35 csbvargi 
 |-  [_ ( 1st ` a ) / x ]_ x = ( 1st ` a )
67 66 eqeq1i 
 |-  ( [_ ( 1st ` a ) / x ]_ x = I <-> ( 1st ` a ) = I )
68 65 67 bitri 
 |-  ( [. ( 1st ` a ) / x ]. x = I <-> ( 1st ` a ) = I )
69 sbcg 
 |-  ( ( 1st ` a ) e. _V -> ( [. ( 1st ` a ) / x ]. ( 2nd ` a ) = J <-> ( 2nd ` a ) = J ) )
70 35 69 ax-mp 
 |-  ( [. ( 1st ` a ) / x ]. ( 2nd ` a ) = J <-> ( 2nd ` a ) = J )
71 68 70 anbi12i 
 |-  ( ( [. ( 1st ` a ) / x ]. x = I /\ [. ( 1st ` a ) / x ]. ( 2nd ` a ) = J ) <-> ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) )
72 63 71 bitri 
 |-  ( [. ( 1st ` a ) / x ]. ( x = I /\ ( 2nd ` a ) = J ) <-> ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) )
73 62 72 anbi12i 
 |-  ( ( [. ( 1st ` a ) / x ]. z e. D /\ [. ( 1st ` a ) / x ]. ( x = I /\ ( 2nd ` a ) = J ) ) <-> ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) )
74 59 60 73 3bitri 
 |-  ( [. ( 1st ` a ) / x ]. [. ( 2nd ` a ) / y ]. ( z e. D /\ ( x = I /\ y = J ) ) <-> ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) )
75 18 43 74 3bitr3g 
 |-  ( ph -> ( ( ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) )
76 75 anbi2d 
 |-  ( ph -> ( ( a e. ( _V X. _V ) /\ ( ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) ) <-> ( a e. ( _V X. _V ) /\ ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) ) )
77 16 76 bitrid 
 |-  ( ph -> ( ( ( a e. ( _V X. _V ) /\ ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( a e. ( _V X. _V ) /\ ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) ) )
78 xpss 
 |-  ( X X. Y ) C_ ( _V X. _V )
79 simprr 
 |-  ( ( ph /\ ( z e. D /\ a = <. I , J >. ) ) -> a = <. I , J >. )
80 9 adantrr 
 |-  ( ( ph /\ ( z e. D /\ a = <. I , J >. ) ) -> <. I , J >. e. ( X X. Y ) )
81 79 80 eqeltrd 
 |-  ( ( ph /\ ( z e. D /\ a = <. I , J >. ) ) -> a e. ( X X. Y ) )
82 78 81 sselid 
 |-  ( ( ph /\ ( z e. D /\ a = <. I , J >. ) ) -> a e. ( _V X. _V ) )
83 82 ex 
 |-  ( ph -> ( ( z e. D /\ a = <. I , J >. ) -> a e. ( _V X. _V ) ) )
84 83 pm4.71rd 
 |-  ( ph -> ( ( z e. D /\ a = <. I , J >. ) <-> ( a e. ( _V X. _V ) /\ ( z e. D /\ a = <. I , J >. ) ) ) )
85 eqop 
 |-  ( a e. ( _V X. _V ) -> ( a = <. I , J >. <-> ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) )
86 85 anbi2d 
 |-  ( a e. ( _V X. _V ) -> ( ( z e. D /\ a = <. I , J >. ) <-> ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) )
87 86 pm5.32i 
 |-  ( ( a e. ( _V X. _V ) /\ ( z e. D /\ a = <. I , J >. ) ) <-> ( a e. ( _V X. _V ) /\ ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) )
88 84 87 bitr2di 
 |-  ( ph -> ( ( a e. ( _V X. _V ) /\ ( z e. D /\ ( ( 1st ` a ) = I /\ ( 2nd ` a ) = J ) ) ) <-> ( z e. D /\ a = <. I , J >. ) ) )
89 77 88 bitrd 
 |-  ( ph -> ( ( ( a e. ( _V X. _V ) /\ ( ( 1st ` a ) e. A /\ ( 2nd ` a ) e. B ) ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( z e. D /\ a = <. I , J >. ) ) )
90 15 89 bitrid 
 |-  ( ph -> ( ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( z e. D /\ a = <. I , J >. ) ) )
91 90 opabbidv 
 |-  ( ph -> { <. z , a >. | ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) } = { <. z , a >. | ( z e. D /\ a = <. I , J >. ) } )
92 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
93 1 92 eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
94 93 cnveqi 
 |-  `' F = `' { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
95 nfv 
 |-  F/ i ( ( x e. A /\ y e. B ) /\ z = C )
96 nfv 
 |-  F/ j ( ( x e. A /\ y e. B ) /\ z = C )
97 nfv 
 |-  F/ x ( i e. A /\ j e. B )
98 nfcsb1v 
 |-  F/_ x [_ i / x ]_ [_ j / y ]_ C
99 98 nfeq2 
 |-  F/ x z = [_ i / x ]_ [_ j / y ]_ C
100 97 99 nfan 
 |-  F/ x ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C )
101 nfv 
 |-  F/ y ( i e. A /\ j e. B )
102 nfcv 
 |-  F/_ y i
103 nfcsb1v 
 |-  F/_ y [_ j / y ]_ C
104 102 103 nfcsbw 
 |-  F/_ y [_ i / x ]_ [_ j / y ]_ C
105 104 nfeq2 
 |-  F/ y z = [_ i / x ]_ [_ j / y ]_ C
106 101 105 nfan 
 |-  F/ y ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C )
107 simpl 
 |-  ( ( x = i /\ y = j ) -> x = i )
108 107 eleq1d 
 |-  ( ( x = i /\ y = j ) -> ( x e. A <-> i e. A ) )
109 simpr 
 |-  ( ( x = i /\ y = j ) -> y = j )
110 109 eleq1d 
 |-  ( ( x = i /\ y = j ) -> ( y e. B <-> j e. B ) )
111 108 110 anbi12d 
 |-  ( ( x = i /\ y = j ) -> ( ( x e. A /\ y e. B ) <-> ( i e. A /\ j e. B ) ) )
112 csbeq1a 
 |-  ( y = j -> C = [_ j / y ]_ C )
113 csbeq1a 
 |-  ( x = i -> [_ j / y ]_ C = [_ i / x ]_ [_ j / y ]_ C )
114 112 113 sylan9eqr 
 |-  ( ( x = i /\ y = j ) -> C = [_ i / x ]_ [_ j / y ]_ C )
115 114 eqeq2d 
 |-  ( ( x = i /\ y = j ) -> ( z = C <-> z = [_ i / x ]_ [_ j / y ]_ C ) )
116 111 115 anbi12d 
 |-  ( ( x = i /\ y = j ) -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C ) ) )
117 95 96 100 106 116 cbvoprab12 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. <. i , j >. , z >. | ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C ) }
118 117 cnveqi 
 |-  `' { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = `' { <. <. i , j >. , z >. | ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C ) }
119 eleq1 
 |-  ( a = <. i , j >. -> ( a e. ( A X. B ) <-> <. i , j >. e. ( A X. B ) ) )
120 opelxp 
 |-  ( <. i , j >. e. ( A X. B ) <-> ( i e. A /\ j e. B ) )
121 119 120 bitrdi 
 |-  ( a = <. i , j >. -> ( a e. ( A X. B ) <-> ( i e. A /\ j e. B ) ) )
122 csbcom 
 |-  [_ ( 2nd ` a ) / j ]_ [_ i / x ]_ [_ j / y ]_ C = [_ i / x ]_ [_ ( 2nd ` a ) / j ]_ [_ j / y ]_ C
123 csbcow 
 |-  [_ ( 2nd ` a ) / j ]_ [_ j / y ]_ C = [_ ( 2nd ` a ) / y ]_ C
124 123 csbeq2i 
 |-  [_ i / x ]_ [_ ( 2nd ` a ) / j ]_ [_ j / y ]_ C = [_ i / x ]_ [_ ( 2nd ` a ) / y ]_ C
125 122 124 eqtri 
 |-  [_ ( 2nd ` a ) / j ]_ [_ i / x ]_ [_ j / y ]_ C = [_ i / x ]_ [_ ( 2nd ` a ) / y ]_ C
126 125 csbeq2i 
 |-  [_ ( 1st ` a ) / i ]_ [_ ( 2nd ` a ) / j ]_ [_ i / x ]_ [_ j / y ]_ C = [_ ( 1st ` a ) / i ]_ [_ i / x ]_ [_ ( 2nd ` a ) / y ]_ C
127 csbcow 
 |-  [_ ( 1st ` a ) / i ]_ [_ i / x ]_ [_ ( 2nd ` a ) / y ]_ C = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C
128 126 127 eqtri 
 |-  [_ ( 1st ` a ) / i ]_ [_ ( 2nd ` a ) / j ]_ [_ i / x ]_ [_ j / y ]_ C = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C
129 csbopeq1a 
 |-  ( a = <. i , j >. -> [_ ( 1st ` a ) / i ]_ [_ ( 2nd ` a ) / j ]_ [_ i / x ]_ [_ j / y ]_ C = [_ i / x ]_ [_ j / y ]_ C )
130 128 129 eqtr3id 
 |-  ( a = <. i , j >. -> [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C = [_ i / x ]_ [_ j / y ]_ C )
131 130 eqeq2d 
 |-  ( a = <. i , j >. -> ( z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C <-> z = [_ i / x ]_ [_ j / y ]_ C ) )
132 121 131 anbi12d 
 |-  ( a = <. i , j >. -> ( ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) <-> ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C ) ) )
133 xpss 
 |-  ( A X. B ) C_ ( _V X. _V )
134 133 sseli 
 |-  ( a e. ( A X. B ) -> a e. ( _V X. _V ) )
135 134 adantr 
 |-  ( ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) -> a e. ( _V X. _V ) )
136 132 135 cnvoprab 
 |-  `' { <. <. i , j >. , z >. | ( ( i e. A /\ j e. B ) /\ z = [_ i / x ]_ [_ j / y ]_ C ) } = { <. z , a >. | ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) }
137 94 118 136 3eqtri 
 |-  `' F = { <. z , a >. | ( a e. ( A X. B ) /\ z = [_ ( 1st ` a ) / x ]_ [_ ( 2nd ` a ) / y ]_ C ) }
138 df-mpt 
 |-  ( z e. D |-> <. I , J >. ) = { <. z , a >. | ( z e. D /\ a = <. I , J >. ) }
139 91 137 138 3eqtr4g 
 |-  ( ph -> `' F = ( z e. D |-> <. I , J >. ) )
140 139 fneq1d 
 |-  ( ph -> ( `' F Fn D <-> ( z e. D |-> <. I , J >. ) Fn D ) )
141 13 140 mpbird 
 |-  ( ph -> `' F Fn D )
142 dff1o4 
 |-  ( F : ( A X. B ) -1-1-onto-> D <-> ( F Fn ( A X. B ) /\ `' F Fn D ) )
143 7 141 142 sylanbrc 
 |-  ( ph -> F : ( A X. B ) -1-1-onto-> D )