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→ 𝐴 )