Metamath Proof Explorer

Theorem pmtrdifwrdellem3

Description: Lemma 3 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 pmtrdifwrdellem3 ⊢W∈WordT→∀i∈0..^W∀n∈N∖KW⁡i⁡n=U⁡i⁡n

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∧i∈0..^W→W⁡i∈T
5 eqid ⊢pmTrsp⁡N⁡dom⁡W⁡i∖I=pmTrsp⁡N⁡dom⁡W⁡i∖I
6 1 2 5 pmtrdifellem3 ⊢W⁡i∈T→∀n∈N∖KW⁡i⁡n=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡n
7 4 6 syl ⊢W∈WordT∧i∈0..^W→∀n∈N∖KW⁡i⁡n=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡n
8 fveq2 ⊢x=i→W⁡x=W⁡i
9 8 difeq1d ⊢x=i→W⁡x∖I=W⁡i∖I
10 9 dmeqd ⊢x=i→dom⁡W⁡x∖I=dom⁡W⁡i∖I
11 10 fveq2d ⊢x=i→pmTrsp⁡N⁡dom⁡W⁡x∖I=pmTrsp⁡N⁡dom⁡W⁡i∖I
12 simpr ⊢W∈WordT∧i∈0..^W→i∈0..^W
13 fvexd ⊢W∈WordT∧i∈0..^W→pmTrsp⁡N⁡dom⁡W⁡i∖I∈V
14 3 11 12 13 fvmptd3 ⊢W∈WordT∧i∈0..^W→U⁡i=pmTrsp⁡N⁡dom⁡W⁡i∖I
15 14 fveq1d ⊢W∈WordT∧i∈0..^W→U⁡i⁡n=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡n
16 15 eqeq2d ⊢W∈WordT∧i∈0..^W→W⁡i⁡n=U⁡i⁡n↔W⁡i⁡n=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡n
17 16 ralbidv ⊢W∈WordT∧i∈0..^W→∀n∈N∖KW⁡i⁡n=U⁡i⁡n↔∀n∈N∖KW⁡i⁡n=pmTrsp⁡N⁡dom⁡W⁡i∖I⁡n
18 7 17 mpbird ⊢W∈WordT∧i∈0..^W→∀n∈N∖KW⁡i⁡n=U⁡i⁡n
19 18 ralrimiva ⊢W∈WordT→∀i∈0..^W∀n∈N∖KW⁡i⁡n=U⁡i⁡n