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

Theorem fin23lem21 8767
 Description: Lemma for fin23 8817. is not empty. We only need here that has at least one set in its range besides ; the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014.) (Revised by Mario Carneiro, 6-May-2015.)
Hypotheses
Ref Expression
fin23lem.a seq𝜔
fin23lem17.f
Assertion
Ref Expression
fin23lem21
Distinct variable groups:   ,,,,,   ,,   ,   ,   ,,,   ,
Allowed substitution hints:   (,,)   (,,,)   (,,,,)

Proof of Theorem fin23lem21
StepHypRef Expression
1 fin23lem.a . . 3 seq𝜔
2 fin23lem17.f . . 3
31, 2fin23lem17 8766 . 2
41fnseqom 7180 . . . . 5
5 fvelrnb 5928 . . . . 5
64, 5ax-mp 5 . . . 4
7 id 23 . . . . . . 7
8 vex 3090 . . . . . . . . . 10
9 f1f1orn 5842 . . . . . . . . . 10
10 f1oen3g 7592 . . . . . . . . . 10
118, 9, 10sylancr 667 . . . . . . . . 9
12 ominf 7790 . . . . . . . . 9
13 ssdif0 3857 . . . . . . . . . . 11
14 snfi 7657 . . . . . . . . . . . . 13
15 ssfi 7798 . . . . . . . . . . . . 13
1614, 15mpan 674 . . . . . . . . . . . 12
17 enfi 7794 . . . . . . . . . . . 12
1816, 17syl5ibr 224 . . . . . . . . . . 11
1913, 18syl5bir 221 . . . . . . . . . 10
2019necon3bd 2643 . . . . . . . . 9
2111, 12, 20mpisyl 22 . . . . . . . 8
22 n0 3777 . . . . . . . . 9
23 eldifsn 4128 . . . . . . . . . . 11
24 elssuni 4251 . . . . . . . . . . . 12
25 ssn0 3801 . . . . . . . . . . . 12
2624, 25sylan 473 . . . . . . . . . . 11
2723, 26sylbi 198 . . . . . . . . . 10
2827exlimiv 1769 . . . . . . . . 9
2922, 28sylbi 198 . . . . . . . 8
3021, 29syl 17 . . . . . . 7
311fin23lem14 8761 . . . . . . 7
327, 30, 31syl2anr 480 . . . . . 6
33 neeq1 2712 . . . . . 6
3432, 33syl5ibcom 223 . . . . 5
3534rexlimdva 2924 . . . 4
366, 35syl5bi 220 . . 3