Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  pwfseqlem2 Structured version   Unicode version

Theorem pwfseqlem2 8534
 Description: Lemma for pwfseq 8539. (Contributed by Mario Carneiro, 18-Nov-2014.)
Hypotheses
Ref Expression
pwfseqlem4.g
pwfseqlem4.x
pwfseqlem4.h
pwfseqlem4.ps
pwfseqlem4.k
pwfseqlem4.d
pwfseqlem4.f
Assertion
Ref Expression
pwfseqlem2
Distinct variable groups:   ,,,,   ,,   ,   ,   ,,,   ,,,,   ,,   ,,,,
Allowed substitution hints:   ()   (,,)   ()   (,,)   (,,,,)   (,,,,)   (,,,)   (,)   (,,,)   (,,,,)   (,,,,)

Proof of Theorem pwfseqlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6088 . . 3
2 fveq2 5728 . . . 4
32fveq2d 5732 . . 3
41, 3eqeq12d 2450 . 2
5 oveq2 6089 . . 3
65eqeq1d 2444 . 2
7 nfcv 2572 . . 3
8 nfcv 2572 . . 3
9 nfcv 2572 . . 3
10 pwfseqlem4.f . . . . . 6
11 nfmpt21 6140 . . . . . 6
1210, 11nfcxfr 2569 . . . . 5
13 nfcv 2572 . . . . 5
147, 12, 13nfov 6104 . . . 4
1514nfeq1 2581 . . 3
16 nfmpt22 6141 . . . . . 6
1710, 16nfcxfr 2569 . . . . 5
188, 17, 9nfov 6104 . . . 4
1918nfeq1 2581 . . 3
20 oveq1 6088 . . . 4
21 fveq2 5728 . . . . 5
2221fveq2d 5732 . . . 4
2320, 22eqeq12d 2450 . . 3
24 oveq2 6089 . . . 4
2524eqeq1d 2444 . . 3
26 vex 2959 . . . . . 6
27 vex 2959 . . . . . 6
28 fvex 5742 . . . . . . 7
29 fvex 5742 . . . . . . 7
3028, 29ifex 3797 . . . . . 6
3110ovmpt4g 6196 . . . . . 6
3226, 27, 30, 31mp3an 1279 . . . . 5
33 iftrue 3745 . . . . 5
3432, 33syl5eq 2480 . . . 4