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 ⊢ ∀ t ∈ T ∃ r ∈ R ∀ x ∈ 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 ∈ T → pmTrsp ⁡ N ⁡ dom ⁡ t ∖ I ∈ R
5 1 2 3 pmtrdifellem3 ⊢ t ∈ T → ∀ x ∈ 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 → ∀ x ∈ N ∖ K t ⁡ x = r ⁡ x ↔ ∀ x ∈ N ∖ K t ⁡ x = pmTrsp ⁡ N ⁡ dom ⁡ t ∖ I ⁡ x
9 8 rspcev ⊢ pmTrsp ⁡ N ⁡ dom ⁡ t ∖ I ∈ R ∧ ∀ x ∈ N ∖ K t ⁡ x = pmTrsp ⁡ N ⁡ dom ⁡ t ∖ I ⁡ x → ∃ r ∈ R ∀ x ∈ N ∖ K t ⁡ x = r ⁡ x
10 4 5 9 syl2anc ⊢ t ∈ T → ∃ r ∈ R ∀ x ∈ N ∖ K t ⁡ x = r ⁡ x
11 10 rgen ⊢ ∀ t ∈ T ∃ r ∈ R ∀ x ∈ N ∖ K t ⁡ x = r ⁡ x