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

Metamath Proof Explorer

Theorem f1o2d2

Description: Sufficient condition for a binary function expressed in maps-to notation to be bijective. (Contributed by SN, 11-Mar-2025)

Ref Expression
Hypotheses f1o2d2.f 
|- F = ( x e. A , y e. B |-> C )
f1o2d2.r 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
f1o2d2.i 
|- ( ( ph /\ z e. D ) -> I e. A )
f1o2d2.j 
|- ( ( ph /\ z e. D ) -> J e. B )
f1o2d2.1 
|- ( ( ph /\ ( ( x e. A /\ y e. B ) /\ z e. D ) ) -> ( ( x = I /\ y = J ) <-> z = C ) )
Assertion f1o2d2 
|- ( ph -> F : ( A X. B ) -1-1-onto-> D )

Proof

Step Hyp Ref Expression
1 f1o2d2.f 
 |-  F = ( x e. A , y e. B |-> C )
2 f1o2d2.r 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C e. D )
3 f1o2d2.i 
 |-  ( ( ph /\ z e. D ) -> I e. A )
4 f1o2d2.j 
 |-  ( ( ph /\ z e. D ) -> J e. B )
5 f1o2d2.1 
 |-  ( ( ph /\ ( ( x e. A /\ y e. B ) /\ z e. D ) ) -> ( ( x = I /\ y = J ) <-> z = C ) )
6 mpompts 
 |-  ( x e. A , y e. B |-> C ) = ( w e. ( A X. B ) |-> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C )
7 1 6 eqtri 
 |-  F = ( w e. ( A X. B ) |-> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C )
8 xp1st 
 |-  ( w e. ( A X. B ) -> ( 1st ` w ) e. A )
9 xp2nd 
 |-  ( w e. ( A X. B ) -> ( 2nd ` w ) e. B )
10 2 anassrs 
 |-  ( ( ( ph /\ x e. A ) /\ y e. B ) -> C e. D )
11 10 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. y e. B C e. D )
12 rspcsbela 
 |-  ( ( ( 2nd ` w ) e. B /\ A. y e. B C e. D ) -> [_ ( 2nd ` w ) / y ]_ C e. D )
13 9 11 12 syl2anr 
 |-  ( ( ( ph /\ x e. A ) /\ w e. ( A X. B ) ) -> [_ ( 2nd ` w ) / y ]_ C e. D )
14 13 an32s 
 |-  ( ( ( ph /\ w e. ( A X. B ) ) /\ x e. A ) -> [_ ( 2nd ` w ) / y ]_ C e. D )
15 14 ralrimiva 
 |-  ( ( ph /\ w e. ( A X. B ) ) -> A. x e. A [_ ( 2nd ` w ) / y ]_ C e. D )
16 rspcsbela 
 |-  ( ( ( 1st ` w ) e. A /\ A. x e. A [_ ( 2nd ` w ) / y ]_ C e. D ) -> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C e. D )
17 8 15 16 syl2an2 
 |-  ( ( ph /\ w e. ( A X. B ) ) -> [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C e. D )
18 3 4 opelxpd 
 |-  ( ( ph /\ z e. D ) -> <. I , J >. e. ( A X. B ) )
19 9 ad2antrl 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( 2nd ` w ) e. B )
20 sbceq2g 
 |-  ( ( 2nd ` w ) e. B -> ( [. ( 2nd ` w ) / y ]. z = C <-> z = [_ ( 2nd ` w ) / y ]_ C ) )
21 19 20 syl 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( [. ( 2nd ` w ) / y ]. z = C <-> z = [_ ( 2nd ` w ) / y ]_ C ) )
22 21 sbcbidv 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. z = C <-> [. ( 1st ` w ) / x ]. z = [_ ( 2nd ` w ) / y ]_ C ) )
23 8 ad2antrl 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( 1st ` w ) e. A )
24 19 adantr 
 |-  ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ x = ( 1st ` w ) ) -> ( 2nd ` w ) e. B )
25 eqop 
 |-  ( w e. ( A X. B ) -> ( w = <. I , J >. <-> ( ( 1st ` w ) = I /\ ( 2nd ` w ) = J ) ) )
26 25 ad2antrl 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( w = <. I , J >. <-> ( ( 1st ` w ) = I /\ ( 2nd ` w ) = J ) ) )
27 eqeq1 
 |-  ( x = ( 1st ` w ) -> ( x = I <-> ( 1st ` w ) = I ) )
28 eqeq1 
 |-  ( y = ( 2nd ` w ) -> ( y = J <-> ( 2nd ` w ) = J ) )
29 27 28 bi2anan9 
 |-  ( ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( ( x = I /\ y = J ) <-> ( ( 1st ` w ) = I /\ ( 2nd ` w ) = J ) ) )
30 29 bicomd 
 |-  ( ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( ( ( 1st ` w ) = I /\ ( 2nd ` w ) = J ) <-> ( x = I /\ y = J ) ) )
31 26 30 sylan9bb 
 |-  ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> ( w = <. I , J >. <-> ( x = I /\ y = J ) ) )
32 31 anassrs 
 |-  ( ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ x = ( 1st ` w ) ) /\ y = ( 2nd ` w ) ) -> ( w = <. I , J >. <-> ( x = I /\ y = J ) ) )
33 eleq1 
 |-  ( x = ( 1st ` w ) -> ( x e. A <-> ( 1st ` w ) e. A ) )
34 8 33 syl5ibrcom 
 |-  ( w e. ( A X. B ) -> ( x = ( 1st ` w ) -> x e. A ) )
35 34 imp 
 |-  ( ( w e. ( A X. B ) /\ x = ( 1st ` w ) ) -> x e. A )
36 eleq1 
 |-  ( y = ( 2nd ` w ) -> ( y e. B <-> ( 2nd ` w ) e. B ) )
37 9 36 syl5ibrcom 
 |-  ( w e. ( A X. B ) -> ( y = ( 2nd ` w ) -> y e. B ) )
38 37 imp 
 |-  ( ( w e. ( A X. B ) /\ y = ( 2nd ` w ) ) -> y e. B )
39 35 38 anim12dan 
 |-  ( ( w e. ( A X. B ) /\ ( x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> ( x e. A /\ y e. B ) )
40 39 3impb 
 |-  ( ( w e. ( A X. B ) /\ x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( x e. A /\ y e. B ) )
41 40 3adant1r 
 |-  ( ( ( w e. ( A X. B ) /\ z e. D ) /\ x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( x e. A /\ y e. B ) )
42 simp1r 
 |-  ( ( ( w e. ( A X. B ) /\ z e. D ) /\ x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> z e. D )
43 41 42 jca 
 |-  ( ( ( w e. ( A X. B ) /\ z e. D ) /\ x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) -> ( ( x e. A /\ y e. B ) /\ z e. D ) )
44 43 5 sylan2 
 |-  ( ( ph /\ ( ( w e. ( A X. B ) /\ z e. D ) /\ x = ( 1st ` w ) /\ y = ( 2nd ` w ) ) ) -> ( ( x = I /\ y = J ) <-> z = C ) )
45 44 3anassrs 
 |-  ( ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ x = ( 1st ` w ) ) /\ y = ( 2nd ` w ) ) -> ( ( x = I /\ y = J ) <-> z = C ) )
46 32 45 bitr2d 
 |-  ( ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ x = ( 1st ` w ) ) /\ y = ( 2nd ` w ) ) -> ( z = C <-> w = <. I , J >. ) )
47 24 46 sbcied 
 |-  ( ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) /\ x = ( 1st ` w ) ) -> ( [. ( 2nd ` w ) / y ]. z = C <-> w = <. I , J >. ) )
48 23 47 sbcied 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( [. ( 1st ` w ) / x ]. [. ( 2nd ` w ) / y ]. z = C <-> w = <. I , J >. ) )
49 sbceq2g 
 |-  ( ( 1st ` w ) e. A -> ( [. ( 1st ` w ) / x ]. z = [_ ( 2nd ` w ) / y ]_ C <-> z = [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C ) )
50 23 49 syl 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( [. ( 1st ` w ) / x ]. z = [_ ( 2nd ` w ) / y ]_ C <-> z = [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C ) )
51 22 48 50 3bitr3d 
 |-  ( ( ph /\ ( w e. ( A X. B ) /\ z e. D ) ) -> ( w = <. I , J >. <-> z = [_ ( 1st ` w ) / x ]_ [_ ( 2nd ` w ) / y ]_ C ) )
52 7 17 18 51 f1o2d 
 |-  ( ph -> F : ( A X. B ) -1-1-onto-> D )