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	$⊢ cf (A) \subseteq card (A)$

Proof

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

Metamath Proof Explorer

Theorem cflecard

Proof