# Metamath Proof Explorer

## Theorem cflm

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of Enderton p. 257. (Contributed by NM, 26-Apr-2004)

Ref Expression
Assertion cflm ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to \mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$

### Proof

Step Hyp Ref Expression
1 elex ${⊢}{A}\in {B}\to {A}\in \mathrm{V}$
2 limsuc ${⊢}\mathrm{Lim}{A}\to \left({v}\in {A}↔\mathrm{suc}{v}\in {A}\right)$
3 2 biimpd ${⊢}\mathrm{Lim}{A}\to \left({v}\in {A}\to \mathrm{suc}{v}\in {A}\right)$
4 sseq1 ${⊢}{z}=\mathrm{suc}{v}\to \left({z}\subseteq {w}↔\mathrm{suc}{v}\subseteq {w}\right)$
5 4 rexbidv ${⊢}{z}=\mathrm{suc}{v}\to \left(\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}↔\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{v}\subseteq {w}\right)$
6 5 rspcv ${⊢}\mathrm{suc}{v}\in {A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{v}\subseteq {w}\right)$
7 sucssel ${⊢}{v}\in \mathrm{V}\to \left(\mathrm{suc}{v}\subseteq {w}\to {v}\in {w}\right)$
8 7 elv ${⊢}\mathrm{suc}{v}\subseteq {w}\to {v}\in {w}$
9 8 reximi ${⊢}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{v}\subseteq {w}\to \exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{v}\in {w}$
10 eluni2 ${⊢}{v}\in \bigcup {y}↔\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{v}\in {w}$
11 9 10 sylibr ${⊢}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{v}\subseteq {w}\to {v}\in \bigcup {y}$
12 6 11 syl6com ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to \left(\mathrm{suc}{v}\in {A}\to {v}\in \bigcup {y}\right)$
13 3 12 syl9 ${⊢}\mathrm{Lim}{A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to \left({v}\in {A}\to {v}\in \bigcup {y}\right)\right)$
14 13 ralrimdv ${⊢}\mathrm{Lim}{A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to \forall {v}\in {A}\phantom{\rule{.4em}{0ex}}{v}\in \bigcup {y}\right)$
15 dfss3 ${⊢}{A}\subseteq \bigcup {y}↔\forall {v}\in {A}\phantom{\rule{.4em}{0ex}}{v}\in \bigcup {y}$
16 14 15 syl6ibr ${⊢}\mathrm{Lim}{A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to {A}\subseteq \bigcup {y}\right)$
17 16 adantr ${⊢}\left(\mathrm{Lim}{A}\wedge {y}\subseteq {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to {A}\subseteq \bigcup {y}\right)$
18 uniss ${⊢}{y}\subseteq {A}\to \bigcup {y}\subseteq \bigcup {A}$
19 limuni ${⊢}\mathrm{Lim}{A}\to {A}=\bigcup {A}$
20 19 sseq2d ${⊢}\mathrm{Lim}{A}\to \left(\bigcup {y}\subseteq {A}↔\bigcup {y}\subseteq \bigcup {A}\right)$
21 18 20 syl5ibr ${⊢}\mathrm{Lim}{A}\to \left({y}\subseteq {A}\to \bigcup {y}\subseteq {A}\right)$
22 21 imp ${⊢}\left(\mathrm{Lim}{A}\wedge {y}\subseteq {A}\right)\to \bigcup {y}\subseteq {A}$
23 17 22 jctird ${⊢}\left(\mathrm{Lim}{A}\wedge {y}\subseteq {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to \left({A}\subseteq \bigcup {y}\wedge \bigcup {y}\subseteq {A}\right)\right)$
24 eqss ${⊢}{A}=\bigcup {y}↔\left({A}\subseteq \bigcup {y}\wedge \bigcup {y}\subseteq {A}\right)$
25 23 24 syl6ibr ${⊢}\left(\mathrm{Lim}{A}\wedge {y}\subseteq {A}\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\to {A}=\bigcup {y}\right)$
26 25 imdistanda ${⊢}\mathrm{Lim}{A}\to \left(\left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\to \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)$
27 26 anim2d ${⊢}\mathrm{Lim}{A}\to \left(\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\to \left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right)$
28 27 eximdv ${⊢}\mathrm{Lim}{A}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right)$
29 28 ss2abdv ${⊢}\mathrm{Lim}{A}\to \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}\subseteq \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$
30 intss ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}\subseteq \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\to \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}$
31 29 30 syl ${⊢}\mathrm{Lim}{A}\to \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}$
32 31 adantl ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}$
33 limelon ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to {A}\in \mathrm{On}$
34 cfval ${⊢}{A}\in \mathrm{On}\to \mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}$
35 33 34 syl ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to \mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right\}$
36 32 35 sseqtrrd ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \mathrm{cf}\left({A}\right)$
37 cfub ${⊢}\mathrm{cf}\left({A}\right)\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)\right\}$
38 eqimss ${⊢}{A}=\bigcup {y}\to {A}\subseteq \bigcup {y}$
39 38 anim2i ${⊢}\left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\to \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)$
40 39 anim2i ${⊢}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\to \left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)$
41 40 eximi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)$
42 41 ss2abi ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)\right\}$
43 intss ${⊢}\left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)\right\}\to \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)\right\}\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$
44 42 43 ax-mp ${⊢}\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}\subseteq \bigcup {y}\right)\right)\right\}\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$
45 37 44 sstri ${⊢}\mathrm{cf}\left({A}\right)\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$
46 36 45 jctil ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to \left(\mathrm{cf}\left({A}\right)\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\wedge \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \mathrm{cf}\left({A}\right)\right)$
47 eqss ${⊢}\mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}↔\left(\mathrm{cf}\left({A}\right)\subseteq \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\wedge \bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}\subseteq \mathrm{cf}\left({A}\right)\right)$
48 46 47 sylibr ${⊢}\left({A}\in \mathrm{V}\wedge \mathrm{Lim}{A}\right)\to \mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$
49 1 48 sylan ${⊢}\left({A}\in {B}\wedge \mathrm{Lim}{A}\right)\to \mathrm{cf}\left({A}\right)=\bigcap \left\{{x}|\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}=\mathrm{card}\left({y}\right)\wedge \left({y}\subseteq {A}\wedge {A}=\bigcup {y}\right)\right)\right\}$