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 syl5eq
 |-  ( ( 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 syl5eq
 |-  ( ( 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 )