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 ( 𝜑𝐴𝑉 )
pmtridf1o.x ( 𝜑𝑋𝐴 )
pmtridf1o.y ( 𝜑𝑌𝐴 )
pmtridf1o.t 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
Assertion pmtridf1o ( 𝜑𝑇 : 𝐴1-1-onto𝐴 )

Proof

Step Hyp Ref Expression
1 pmtridf1o.a ( 𝜑𝐴𝑉 )
2 pmtridf1o.x ( 𝜑𝑋𝐴 )
3 pmtridf1o.y ( 𝜑𝑌𝐴 )
4 pmtridf1o.t 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
5 iftrue ( 𝑋 = 𝑌 → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( I ↾ 𝐴 ) )
6 5 adantl ( ( 𝜑𝑋 = 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( I ↾ 𝐴 ) )
7 4 6 syl5eq ( ( 𝜑𝑋 = 𝑌 ) → 𝑇 = ( I ↾ 𝐴 ) )
8 f1oi ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴
9 8 a1i ( ( 𝜑𝑋 = 𝑌 ) → ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴 )
10 f1oeq1 ( 𝑇 = ( I ↾ 𝐴 ) → ( 𝑇 : 𝐴1-1-onto𝐴 ↔ ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴 ) )
11 10 biimpar ( ( 𝑇 = ( I ↾ 𝐴 ) ∧ ( I ↾ 𝐴 ) : 𝐴1-1-onto𝐴 ) → 𝑇 : 𝐴1-1-onto𝐴 )
12 7 9 11 syl2anc ( ( 𝜑𝑋 = 𝑌 ) → 𝑇 : 𝐴1-1-onto𝐴 )
13 simpr ( ( 𝜑𝑋𝑌 ) → 𝑋𝑌 )
14 13 neneqd ( ( 𝜑𝑋𝑌 ) → ¬ 𝑋 = 𝑌 )
15 iffalse ( ¬ 𝑋 = 𝑌 → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
16 14 15 syl ( ( 𝜑𝑋𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
17 4 16 syl5eq ( ( 𝜑𝑋𝑌 ) → 𝑇 = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
18 1 adantr ( ( 𝜑𝑋𝑌 ) → 𝐴𝑉 )
19 2 adantr ( ( 𝜑𝑋𝑌 ) → 𝑋𝐴 )
20 3 adantr ( ( 𝜑𝑋𝑌 ) → 𝑌𝐴 )
21 19 20 prssd ( ( 𝜑𝑋𝑌 ) → { 𝑋 , 𝑌 } ⊆ 𝐴 )
22 pr2nelem ( ( 𝑋𝐴𝑌𝐴𝑋𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
23 19 20 13 22 syl3anc ( ( 𝜑𝑋𝑌 ) → { 𝑋 , 𝑌 } ≈ 2o )
24 eqid ( pmTrsp ‘ 𝐴 ) = ( pmTrsp ‘ 𝐴 )
25 eqid ran ( pmTrsp ‘ 𝐴 ) = ran ( pmTrsp ‘ 𝐴 )
26 24 25 pmtrrn ( ( 𝐴𝑉 ∧ { 𝑋 , 𝑌 } ⊆ 𝐴 ∧ { 𝑋 , 𝑌 } ≈ 2o ) → ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ∈ ran ( pmTrsp ‘ 𝐴 ) )
27 18 21 23 26 syl3anc ( ( 𝜑𝑋𝑌 ) → ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ∈ ran ( pmTrsp ‘ 𝐴 ) )
28 17 27 eqeltrd ( ( 𝜑𝑋𝑌 ) → 𝑇 ∈ ran ( pmTrsp ‘ 𝐴 ) )
29 24 25 pmtrff1o ( 𝑇 ∈ ran ( pmTrsp ‘ 𝐴 ) → 𝑇 : 𝐴1-1-onto𝐴 )
30 28 29 syl ( ( 𝜑𝑋𝑌 ) → 𝑇 : 𝐴1-1-onto𝐴 )
31 12 30 pm2.61dane ( 𝜑𝑇 : 𝐴1-1-onto𝐴 )