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