Description: A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set A . (Contributed by NM, 24-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 25-Jul-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | cflem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssid | |
|
2 | ssid | |
|
3 | sseq2 | |
|
4 | 3 | rspcev | |
5 | 2 4 | mpan2 | |
6 | 5 | rgen | |
7 | sseq1 | |
|
8 | rexeq | |
|
9 | 8 | ralbidv | |
10 | 7 9 | anbi12d | |
11 | 10 | spcegv | |
12 | 1 6 11 | mp2ani | |
13 | fvex | |
|
14 | 13 | isseti | |
15 | 19.41v | |
|
16 | 14 15 | mpbiran | |
17 | 16 | exbii | |
18 | fveq2 | |
|
19 | 18 | eqeq2d | |
20 | sseq1 | |
|
21 | rexeq | |
|
22 | 21 | ralbidv | |
23 | 20 22 | anbi12d | |
24 | 19 23 | anbi12d | |
25 | 24 | excomimw | |
26 | 17 25 | sylbir | |
27 | 12 26 | syl | |