Description: The beginning of the proof that every II-finite set (every chain of subsets has a maximal element) is III-finite (has no denumerable collection of subsets).
This first section is dedicated to the construction of U and its intersection. First, the value of U at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fin23lem.a | |
|
Assertion | fin23lem12 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fin23lem.a | |
|
2 | 1 | seqomsuc | |
3 | fvex | |
|
4 | fveq2 | |
|
5 | 4 | ineq1d | |
6 | 5 | eqeq1d | |
7 | 6 5 | ifbieq2d | |
8 | ineq2 | |
|
9 | 8 | eqeq1d | |
10 | id | |
|
11 | 9 10 8 | ifbieq12d | |
12 | eqid | |
|
13 | 3 | inex2 | |
14 | 3 13 | ifex | |
15 | 7 11 12 14 | ovmpo | |
16 | 3 15 | mpan2 | |
17 | 2 16 | eqtrd | |