Theorem pmtridfv1

Description: Value at X of the transposition of X and Y (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022)

	Ref	Expression
Hypotheses	pmtridf1o.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	pmtridf1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	pmtridf1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
	pmtridf1o.t	⊢ 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
Assertion	pmtridfv1	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑋 ) = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		pmtridf1o.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		pmtridf1o.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
3		pmtridf1o.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐴 )
4		pmtridf1o.t	⊢ 𝑇 = if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
5		simpr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑋 = 𝑌 )
6	5	iftrued	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( I ↾ 𝐴 ) )
7	4 6	syl5eq	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → 𝑇 = ( I ↾ 𝐴 ) )
8	7	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑇 ‘ 𝑋 ) = ( ( I ↾ 𝐴 ) ‘ 𝑋 ) )
9		fvresi	⊢ ( 𝑋 ∈ 𝐴 → ( ( I ↾ 𝐴 ) ‘ 𝑋 ) = 𝑋 )
10	2 9	syl	⊢ ( 𝜑 → ( ( I ↾ 𝐴 ) ‘ 𝑋 ) = 𝑋 )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( ( I ↾ 𝐴 ) ‘ 𝑋 ) = 𝑋 )
12	8 11 5	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 = 𝑌 ) → ( 𝑇 ‘ 𝑋 ) = 𝑌 )
13		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ≠ 𝑌 )
14	13	neneqd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ¬ 𝑋 = 𝑌 )
15	14	iffalsed	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → if ( 𝑋 = 𝑌 , ( I ↾ 𝐴 ) , ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ) = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
16	4 15	syl5eq	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑇 = ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) )
17	16	fveq1d	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑇 ‘ 𝑋 ) = ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) )
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝐴 ∈ 𝑉 )
19	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝐴 )
20	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ 𝐴 )
21		eqid	⊢ ( pmTrsp ‘ 𝐴 ) = ( pmTrsp ‘ 𝐴 )
22	21	pmtrprfv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ≠ 𝑌 ) ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )
23	18 19 20 13 22	syl13anc	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( pmTrsp ‘ 𝐴 ) ‘ { 𝑋 , 𝑌 } ) ‘ 𝑋 ) = 𝑌 )
24	17 23	eqtrd	⊢ ( ( 𝜑 ∧ 𝑋 ≠ 𝑌 ) → ( 𝑇 ‘ 𝑋 ) = 𝑌 )
25	12 24	pm2.61dane	⊢ ( 𝜑 → ( 𝑇 ‘ 𝑋 ) = 𝑌 )