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

Theorem fin23lem29 8221
 Description: Lemma for fin23 8269. The residual is built from the same elements as the previous sequence. (Contributed by Stefan O'Rear, 2-Nov-2014.)
Hypotheses
Ref Expression
fin23lem.a seq𝜔
fin23lem17.f
fin23lem.b
fin23lem.c
fin23lem.d
fin23lem.e
Assertion
Ref Expression
fin23lem29
Distinct variable groups:   ,,,,,,,   ,,   ,,,,   ,,,,   ,,,,,   ,   ,
Allowed substitution hints:   (,,,,)   (,,,,,,,,)   (,,,,)   (,,,)   (,,,,,,)   (,,,,,,,)

Proof of Theorem fin23lem29
StepHypRef Expression
1 fin23lem.e . 2
2 eqif 3772 . . 3
32biimpi 187 . 2
4 rneq 5095 . . . . . 6
54unieqd 4026 . . . . 5
6 rncoss 5136 . . . . . 6
76unissi 4038 . . . . 5
85, 7syl6eqss 3398 . . . 4
10 rneq 5095 . . . . . 6
1110unieqd 4026 . . . . 5
12 rncoss 5136 . . . . . . 7
1312unissi 4038 . . . . . 6
14 unissb 4045 . . . . . . 7
15 abid 2424 . . . . . . . . 9
16 fvssunirn 5754 . . . . . . . . . . . . 13
1716a1i 11 . . . . . . . . . . . 12
1817ssdifssd 3485 . . . . . . . . . . 11
19 sseq1 3369 . . . . . . . . . . 11
2018, 19syl5ibrcom 214 . . . . . . . . . 10
2120rexlimiv 2824 . . . . . . . . 9
2215, 21sylbi 188 . . . . . . . 8
23 eqid 2436 . . . . . . . . 9
2423rnmpt 5116 . . . . . . . 8
2522, 24eleq2s 2528 . . . . . . 7
2614, 25mprgbir 2776 . . . . . 6
2713, 26sstri 3357 . . . . 5
2811, 27syl6eqss 3398 . . . 4