Description: Lemma for fin23 . U will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fin23lem.a | |
|
Assertion | fin23lem14 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fin23lem.a | |
|
2 | fveq2 | |
|
3 | 2 | neeq1d | |
4 | 3 | imbi2d | |
5 | fveq2 | |
|
6 | 5 | neeq1d | |
7 | 6 | imbi2d | |
8 | fveq2 | |
|
9 | 8 | neeq1d | |
10 | 9 | imbi2d | |
11 | fveq2 | |
|
12 | 11 | neeq1d | |
13 | 12 | imbi2d | |
14 | vex | |
|
15 | 14 | rnex | |
16 | 15 | uniex | |
17 | 1 | seqom0g | |
18 | 16 17 | mp1i | |
19 | id | |
|
20 | 18 19 | eqnetrd | |
21 | 1 | fin23lem12 | |
22 | 21 | adantr | |
23 | iftrue | |
|
24 | 23 | adantr | |
25 | simprr | |
|
26 | 24 25 | eqnetrd | |
27 | iffalse | |
|
28 | 27 | adantr | |
29 | neqne | |
|
30 | 29 | adantr | |
31 | 28 30 | eqnetrd | |
32 | 26 31 | pm2.61ian | |
33 | 22 32 | eqnetrd | |
34 | 33 | ex | |
35 | 34 | imim2d | |
36 | 4 7 10 13 20 35 | finds | |
37 | 36 | imp | |