# Metamath Proof Explorer

## Theorem cflecard

Description: Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cflecard ${⊢}\mathrm{cf}\left({A}\right)\subseteq \mathrm{card}\left({A}\right)$

### Proof

Step Hyp Ref Expression
1 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\}$
2 df-sn ${⊢}\left\{\mathrm{card}\left({A}\right)\right\}=\left\{{x}|{x}=\mathrm{card}\left({A}\right)\right\}$
3 ssid ${⊢}{A}\subseteq {A}$
4 ssid ${⊢}{z}\subseteq {z}$
5 sseq2 ${⊢}{w}={z}\to \left({z}\subseteq {w}↔{z}\subseteq {z}\right)$
6 5 rspcev ${⊢}\left({z}\in {A}\wedge {z}\subseteq {z}\right)\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
7 4 6 mpan2 ${⊢}{z}\in {A}\to \exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
8 7 rgen ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}$
9 3 8 pm3.2i ${⊢}\left({A}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)$
10 fveq2 ${⊢}{y}={A}\to \mathrm{card}\left({y}\right)=\mathrm{card}\left({A}\right)$
11 10 eqeq2d ${⊢}{y}={A}\to \left({x}=\mathrm{card}\left({y}\right)↔{x}=\mathrm{card}\left({A}\right)\right)$
12 sseq1 ${⊢}{y}={A}\to \left({y}\subseteq {A}↔{A}\subseteq {A}\right)$
13 rexeq ${⊢}{y}={A}\to \left(\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}↔\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)$
14 13 ralbidv ${⊢}{y}={A}\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)$
15 12 14 anbi12d ${⊢}{y}={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)↔\left({A}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)$
16 11 15 anbi12d ${⊢}{y}={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)↔\left({x}=\mathrm{card}\left({A}\right)\wedge \left({A}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right)$
17 16 spcegv ${⊢}{A}\in \mathrm{On}\to \left(\left({x}=\mathrm{card}\left({A}\right)\wedge \left({A}\subseteq {A}\wedge \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {A}\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 \forall {z}\in {A}\phantom{\rule{.4em}{0ex}}\exists {w}\in {y}\phantom{\rule{.4em}{0ex}}{z}\subseteq {w}\right)\right)\right)$
18 9 17 mpan2i ${⊢}{A}\in \mathrm{On}\to \left({x}=\mathrm{card}\left({A}\right)\to \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)$
19 18 ss2abdv ${⊢}{A}\in \mathrm{On}\to \left\{{x}|{x}=\mathrm{card}\left({A}\right)\right\}\subseteq \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\}$
20 2 19 eqsstrid ${⊢}{A}\in \mathrm{On}\to \left\{\mathrm{card}\left({A}\right)\right\}\subseteq \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\}$
21 intss ${⊢}\left\{\mathrm{card}\left({A}\right)\right\}\subseteq \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\}\to \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\}\subseteq \bigcap \left\{\mathrm{card}\left({A}\right)\right\}$
22 20 21 syl ${⊢}{A}\in \mathrm{On}\to \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\}\subseteq \bigcap \left\{\mathrm{card}\left({A}\right)\right\}$
23 fvex ${⊢}\mathrm{card}\left({A}\right)\in \mathrm{V}$
24 23 intsn ${⊢}\bigcap \left\{\mathrm{card}\left({A}\right)\right\}=\mathrm{card}\left({A}\right)$
25 22 24 sseqtrdi ${⊢}{A}\in \mathrm{On}\to \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\}\subseteq \mathrm{card}\left({A}\right)$
26 1 25 eqsstrd ${⊢}{A}\in \mathrm{On}\to \mathrm{cf}\left({A}\right)\subseteq \mathrm{card}\left({A}\right)$
27 cff ${⊢}\mathrm{cf}:\mathrm{On}⟶\mathrm{On}$
28 27 fdmi ${⊢}\mathrm{dom}\mathrm{cf}=\mathrm{On}$
29 28 eleq2i ${⊢}{A}\in \mathrm{dom}\mathrm{cf}↔{A}\in \mathrm{On}$
30 ndmfv ${⊢}¬{A}\in \mathrm{dom}\mathrm{cf}\to \mathrm{cf}\left({A}\right)=\varnothing$
31 29 30 sylnbir ${⊢}¬{A}\in \mathrm{On}\to \mathrm{cf}\left({A}\right)=\varnothing$
32 0ss ${⊢}\varnothing \subseteq \mathrm{card}\left({A}\right)$
33 31 32 eqsstrdi ${⊢}¬{A}\in \mathrm{On}\to \mathrm{cf}\left({A}\right)\subseteq \mathrm{card}\left({A}\right)$
34 26 33 pm2.61i ${⊢}\mathrm{cf}\left({A}\right)\subseteq \mathrm{card}\left({A}\right)$