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

Theorem fin23lem39 8230
 Description: Lemma for fin23 8269. Thus, we have that could not have been in after all. (Contributed by Stefan O'Rear, 4-Nov-2014.)
Hypotheses
Ref Expression
fin23lem33.f
fin23lem.f
fin23lem.g
fin23lem.h
fin23lem.i
Assertion
Ref Expression
fin23lem39
Distinct variable groups:   ,,,,,,   ,   ,,   ,,
Allowed substitution hints:   (,,,)   (,,,,)   (,,,)

Proof of Theorem fin23lem39
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fin23lem33.f . . 3
2 fin23lem.f . . 3
3 fin23lem.g . . 3
4 fin23lem.h . . 3
5 fin23lem.i . . 3
61, 2, 3, 4, 5fin23lem38 8229 . 2
71, 2, 3, 4, 5fin23lem34 8226 . . . . . . . 8
87simprd 450 . . . . . . 7
98adantlr 696 . . . . . 6
10 elpw2g 4363 . . . . . . 7
1110ad2antlr 708 . . . . . 6
129, 11mpbird 224 . . . . 5
13 eqid 2436 . . . . 5
1412, 13fmptd 5893 . . . 4
15 pwexg 4383 . . . . 5
16 vex 2959 . . . . . . 7
17 f1f 5639 . . . . . . 7
18 dmfex 5626 . . . . . . 7
1916, 17, 18sylancr 645 . . . . . 6
202, 19syl 16 . . . . 5
21 elmapg 7031 . . . . 5
2215, 20, 21syl2anr 465 . . . 4
2314, 22mpbird 224 . . 3
241isfin3ds 8209 . . . . 5
2524ibi 233 . . . 4
271, 2, 3, 4, 5fin23lem35 8227 . . . . . . 7
2827pssssd 3444 . . . . . 6
29 peano2 4865 . . . . . . . . 9
30 fveq2 5728 . . . . . . . . . . . 12
3130rneqd 5097 . . . . . . . . . . 11
3231unieqd 4026 . . . . . . . . . 10
33 fvex 5742 . . . . . . . . . . . 12
3433rnex 5133 . . . . . . . . . . 11
3534uniex 4705 . . . . . . . . . 10
3632, 13, 35fvmpt 5806 . . . . . . . . 9
3729, 36syl 16 . . . . . . . 8
38 fveq2 5728 . . . . . . . . . . 11
3938rneqd 5097 . . . . . . . . . 10
4039unieqd 4026 . . . . . . . . 9
41 fvex 5742 . . . . . . . . . . 11
4241rnex 5133 . . . . . . . . . 10
4342uniex 4705 . . . . . . . . 9
4440, 13, 43fvmpt 5806 . . . . . . . 8
4537, 44sseq12d 3377 . . . . . . 7
4645adantl 453 . . . . . 6
4728, 46mpbird 224 . . . . 5
4847ralrimiva 2789 . . . 4