Metamath Proof Explorer

Theorem pmtridf1o

Description: Transpositions of X and Y (understood to be the identity when X = Y ), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Hypotheses pmtridf1o.a 
|- ( ph -> A e. V )
pmtridf1o.x 
|- ( ph -> X e. A )
pmtridf1o.y 
|- ( ph -> Y e. A )
pmtridf1o.t 
|- T = if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) )
Assertion pmtridf1o 
|- ( ph -> T : A -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 pmtridf1o.a 
 |-  ( ph -> A e. V )
2 pmtridf1o.x 
 |-  ( ph -> X e. A )
3 pmtridf1o.y 
 |-  ( ph -> Y e. A )
4 pmtridf1o.t 
 |-  T = if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) )
5 iftrue 
 |-  ( X = Y -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( _I |` A ) )
6 5 adantl 
 |-  ( ( ph /\ X = Y ) -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( _I |` A ) )
7 4 6 eqtrid 
 |-  ( ( ph /\ X = Y ) -> T = ( _I |` A ) )
8 f1oi 
 |-  ( _I |` A ) : A -1-1-onto-> A
9 8 a1i 
 |-  ( ( ph /\ X = Y ) -> ( _I |` A ) : A -1-1-onto-> A )
10 f1oeq1 
 |-  ( T = ( _I |` A ) -> ( T : A -1-1-onto-> A <-> ( _I |` A ) : A -1-1-onto-> A ) )
11 10 biimpar 
 |-  ( ( T = ( _I |` A ) /\ ( _I |` A ) : A -1-1-onto-> A ) -> T : A -1-1-onto-> A )
12 7 9 11 syl2anc 
 |-  ( ( ph /\ X = Y ) -> T : A -1-1-onto-> A )
13 simpr 
 |-  ( ( ph /\ X =/= Y ) -> X =/= Y )
14 13 neneqd 
 |-  ( ( ph /\ X =/= Y ) -> -. X = Y )
15 iffalse 
 |-  ( -. X = Y -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( ( pmTrsp ` A ) ` { X , Y } ) )
16 14 15 syl 
 |-  ( ( ph /\ X =/= Y ) -> if ( X = Y , ( _I |` A ) , ( ( pmTrsp ` A ) ` { X , Y } ) ) = ( ( pmTrsp ` A ) ` { X , Y } ) )
17 4 16 eqtrid 
 |-  ( ( ph /\ X =/= Y ) -> T = ( ( pmTrsp ` A ) ` { X , Y } ) )
18 1 adantr 
 |-  ( ( ph /\ X =/= Y ) -> A e. V )
19 2 adantr 
 |-  ( ( ph /\ X =/= Y ) -> X e. A )
20 3 adantr 
 |-  ( ( ph /\ X =/= Y ) -> Y e. A )
21 19 20 prssd 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } C_ A )
22 pr2nelem 
 |-  ( ( X e. A /\ Y e. A /\ X =/= Y ) -> { X , Y } ~~ 2o )
23 19 20 13 22 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> { X , Y } ~~ 2o )
24 eqid 
 |-  ( pmTrsp ` A ) = ( pmTrsp ` A )
25 eqid 
 |-  ran ( pmTrsp ` A ) = ran ( pmTrsp ` A )
26 24 25 pmtrrn 
 |-  ( ( A e. V /\ { X , Y } C_ A /\ { X , Y } ~~ 2o ) -> ( ( pmTrsp ` A ) ` { X , Y } ) e. ran ( pmTrsp ` A ) )
27 18 21 23 26 syl3anc 
 |-  ( ( ph /\ X =/= Y ) -> ( ( pmTrsp ` A ) ` { X , Y } ) e. ran ( pmTrsp ` A ) )
28 17 27 eqeltrd 
 |-  ( ( ph /\ X =/= Y ) -> T e. ran ( pmTrsp ` A ) )
29 24 25 pmtrff1o 
 |-  ( T e. ran ( pmTrsp ` A ) -> T : A -1-1-onto-> A )
30 28 29 syl 
 |-  ( ( ph /\ X =/= Y ) -> T : A -1-1-onto-> A )
31 12 30 pm2.61dane 
 |-  ( ph -> T : A -1-1-onto-> A )