Metamath Proof Explorer

Theorem pmtrdifwrdellem1

Description: Lemma 1 for pmtrdifwrdel . (Contributed by AV, 15-Jan-2019)

Ref Expression
Hypotheses pmtrdifel.t ⊢ T = ran ⁡ pmTrsp ⁡ N ∖ K
pmtrdifel.r ⊢ R = ran ⁡ pmTrsp ⁡ N
pmtrdifwrdel.0 ⊢ U = x ∈ 0 ..^ W ⟼ pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I
Assertion pmtrdifwrdellem1 ⊢ W ∈ Word T → U ∈ Word R

Proof

Step Hyp Ref Expression
1 pmtrdifel.t ⊢ T = ran ⁡ pmTrsp ⁡ N ∖ K
2 pmtrdifel.r ⊢ R = ran ⁡ pmTrsp ⁡ N
3 pmtrdifwrdel.0 ⊢ U = x ∈ 0 ..^ W ⟼ pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I
4 wrdsymbcl ⊢ W ∈ Word T ∧ x ∈ 0 ..^ W → W ⁡ x ∈ T
5 eqid ⊢ pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I = pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I
6 1 2 5 pmtrdifellem1 ⊢ W ⁡ x ∈ T → pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I ∈ R
7 4 6 syl ⊢ W ∈ Word T ∧ x ∈ 0 ..^ W → pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I ∈ R
8 7 3 fmptd ⊢ W ∈ Word T → U : 0 ..^ W ⟶ R
9 iswrdi ⊢ U : 0 ..^ W ⟶ R → U ∈ Word R
10 8 9 syl ⊢ W ∈ Word T → U ∈ Word R