cfub

Description: An upper bound on cofinality. (Contributed by NM, 25-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Assertion	cfub	$⊢ cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$

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		dfss3	$⊢ A \subseteq ⋃ y \leftrightarrow \forall z \in A z \in ⋃ y$
3		ssel	$⊢ y \subseteq A \to (w \in y \to w \in A)$
4		onelon	$⊢ (A \in On \land w \in A) \to w \in On$
5	4	ex	$⊢ A \in On \to (w \in A \to w \in On)$
6	3 5	sylan9r	$⊢ (A \in On \land y \subseteq A) \to (w \in y \to w \in On)$
7		onelss	$⊢ w \in On \to (z \in w \to z \subseteq w)$
8	6 7	syl6	$⊢ (A \in On \land y \subseteq A) \to (w \in y \to (z \in w \to z \subseteq w))$
9	8	imdistand	$⊢ (A \in On \land y \subseteq A) \to ((w \in y \land z \in w) \to (w \in y \land z \subseteq w))$
10	9	ancomsd	$⊢ (A \in On \land y \subseteq A) \to ((z \in w \land w \in y) \to (w \in y \land z \subseteq w))$
11	10	eximdv	$⊢ (A \in On \land y \subseteq A) \to (\exists w (z \in w \land w \in y) \to \exists w (w \in y \land z \subseteq w))$
12		eluni	$⊢ z \in ⋃ y \leftrightarrow \exists w (z \in w \land w \in y)$
13		df-rex	$⊢ \exists w \in y z \subseteq w \leftrightarrow \exists w (w \in y \land z \subseteq w)$
14	11 12 13	3imtr4g	$⊢ (A \in On \land y \subseteq A) \to (z \in ⋃ y \to \exists w \in y z \subseteq w)$
15	14	ralimdv	$⊢ (A \in On \land y \subseteq A) \to (\forall z \in A z \in ⋃ y \to \forall z \in A \exists w \in y z \subseteq w)$
16	2 15	biimtrid	$⊢ (A \in On \land y \subseteq A) \to (A \subseteq ⋃ y \to \forall z \in A \exists w \in y z \subseteq w)$
17	16	imdistanda	$⊢ A \in On \to ((y \subseteq A \land A \subseteq ⋃ y) \to (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
18	17	anim2d	$⊢ A \in On \to ((x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y)) \to (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
19	18	eximdv	$⊢ A \in On \to (\exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y)) \to \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
20	19	ss2abdv	$⊢ A \in On \to \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\} \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	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\} \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 ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
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 ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
23	1 22	eqsstrd	$⊢ A \in On \to cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
24		cff	$⊢ cf : On ⟶ On$
25	24	fdmi	$⊢ dom cf = On$
26	25	eleq2i	$⊢ A \in dom cf \leftrightarrow A \in On$
27		ndmfv	$⊢ \neg A \in dom cf \to cf (A) = \emptyset$
28	26 27	sylnbir	$⊢ \neg A \in On \to cf (A) = \emptyset$
29		0ss	$⊢ \emptyset \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
30	28 29	eqsstrdi	$⊢ \neg A \in On \to cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
31	23 30	pm2.61i	$⊢ cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$

Metamath Proof Explorer

Theorem cfub

Proof