Theorem pmtrdifel

Description: A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019)

	Ref	Expression
Hypotheses	pmtrdifel.t	|- T = ran ( pmTrsp ` ( N \ { K } ) )
	pmtrdifel.r	|- R = ran ( pmTrsp ` N )
Assertion	pmtrdifel	|- A. t e. T E. r e. R A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x )

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	|- T = ran ( pmTrsp ` ( N \ { K } ) )
2		pmtrdifel.r	|- R = ran ( pmTrsp ` N )
3		eqid	|- ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) = ( ( pmTrsp ` N ) ` dom ( t \ _I ) )
4	1 2 3	pmtrdifellem1	|- ( t e. T -> ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) e. R )
5	1 2 3	pmtrdifellem3	|- ( t e. T -> A. x e. ( N \ { K } ) ( t ` x ) = ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) ` x ) )
6		fveq1	|- ( r = ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) -> ( r ` x ) = ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) ` x ) )
7	6	eqeq2d	|- ( r = ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) -> ( ( t ` x ) = ( r ` x ) <-> ( t ` x ) = ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) ` x ) ) )
8	7	ralbidv	|- ( r = ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) -> ( A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x ) <-> A. x e. ( N \ { K } ) ( t ` x ) = ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) ` x ) ) )
9	8	rspcev	|- ( ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) e. R /\ A. x e. ( N \ { K } ) ( t ` x ) = ( ( ( pmTrsp ` N ) ` dom ( t \ _I ) ) ` x ) ) -> E. r e. R A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x ) )
10	4 5 9	syl2anc	|- ( t e. T -> E. r e. R A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x ) )
11	10	rgen	|- A. t e. T E. r e. R A. x e. ( N \ { K } ) ( t ` x ) = ( r ` x )