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