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

Metamath Proof Explorer

Theorem pmtrdifwrdellem2

Description: Lemma 2 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 pmtrdifwrdellem2 ⊢ W ∈ Word T → W = U

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 ralrimiva ⊢ W ∈ Word T → ∀ x ∈ 0 ..^ W pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I ∈ R
9 3 fnmpt ⊢ ∀ x ∈ 0 ..^ W pmTrsp ⁡ N ⁡ dom ⁡ W ⁡ x ∖ I ∈ R → U Fn 0 ..^ W
10 hashfn ⊢ U Fn 0 ..^ W → U = 0 ..^ W
11 8 9 10 3syl ⊢ W ∈ Word T → U = 0 ..^ W
12 lencl ⊢ W ∈ Word T → W ∈ ℕ 0
13 hashfzo0 ⊢ W ∈ ℕ 0 → 0 ..^ W = W
14 12 13 syl ⊢ W ∈ Word T → 0 ..^ W = W
15 11 14 eqtr2d ⊢ W ∈ Word T → W = U