This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )