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	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
	pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
Assertion	pmtrdifel	⊢ ∀ 𝑡 ∈ 𝑇 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		pmtrdifel.t	⊢ 𝑇 = ran ( pmTrsp ‘ ( 𝑁 ∖ { 𝐾 } ) )
2		pmtrdifel.r	⊢ 𝑅 = ran ( pmTrsp ‘ 𝑁 )
3		eqid	⊢ ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) )
4	1 2 3	pmtrdifellem1	⊢ ( 𝑡 ∈ 𝑇 → ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ∈ 𝑅 )
5	1 2 3	pmtrdifellem3	⊢ ( 𝑡 ∈ 𝑇 → ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ‘ 𝑥 ) )
6		fveq1	⊢ ( 𝑟 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) → ( 𝑟 ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ‘ 𝑥 ) )
7	6	eqeq2d	⊢ ( 𝑟 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) → ( ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 ) ↔ ( 𝑡 ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ‘ 𝑥 ) ) )
8	7	ralbidv	⊢ ( 𝑟 = ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) → ( ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ‘ 𝑥 ) ) )
9	8	rspcev	⊢ ( ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ∈ 𝑅 ∧ ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( ( ( pmTrsp ‘ 𝑁 ) ‘ dom ( 𝑡 ∖ I ) ) ‘ 𝑥 ) ) → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 ) )
10	4 5 9	syl2anc	⊢ ( 𝑡 ∈ 𝑇 → ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 ) )
11	10	rgen	⊢ ∀ 𝑡 ∈ 𝑇 ∃ 𝑟 ∈ 𝑅 ∀ 𝑥 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝑡 ‘ 𝑥 ) = ( 𝑟 ‘ 𝑥 )