cflem

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	$⊢ A \in V \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ A \subseteq A$
2		ssid	$⊢ z \subseteq z$
3		sseq2	$⊢ w = z \to (z \subseteq w \leftrightarrow z \subseteq z)$
4	3	rspcev	$⊢ (z \in A \land z \subseteq z) \to \exists w \in A z \subseteq w$
5	2 4	mpan2	$⊢ z \in A \to \exists w \in A z \subseteq w$
6	5	rgen	$⊢ \forall z \in A \exists w \in A z \subseteq w$
7		sseq1	$⊢ y = A \to (y \subseteq A \leftrightarrow A \subseteq A)$
8		rexeq	$⊢ y = A \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in A z \subseteq w)$
9	8	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)$
10	7 9	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))$
11	10	spcegv	$⊢ A \in V \to ((A \subseteq A \land \forall z \in A \exists w \in A z \subseteq w) \to \exists y (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
12	1 6 11	mp2ani	$⊢ A \in V \to \exists y (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)$
13		fvex	$⊢ card (y) \in V$
14	13	isseti	$⊢ \exists x x = card (y)$
15		19.41v	$⊢ \exists x (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow (\exists x x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
16	14 15	mpbiran	$⊢ \exists x (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)$
17	16	exbii	$⊢ \exists y \exists x (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow \exists y (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)$
18		fveq2	$⊢ y = v \to card (y) = card (v)$
19	18	eqeq2d	$⊢ y = v \to (x = card (y) \leftrightarrow x = card (v))$
20		sseq1	$⊢ y = v \to (y \subseteq A \leftrightarrow v \subseteq A)$
21		rexeq	$⊢ y = v \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in v z \subseteq w)$
22	21	ralbidv	$⊢ y = v \to (\forall z \in A \exists w \in y z \subseteq w \leftrightarrow \forall z \in A \exists w \in v z \subseteq w)$
23	20 22	anbi12d	$⊢ y = v \to ((y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w) \leftrightarrow (v \subseteq A \land \forall z \in A \exists w \in v z \subseteq w))$
24	19 23	anbi12d	$⊢ y = v \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow (x = card (v) \land (v \subseteq A \land \forall z \in A \exists w \in v z \subseteq w)))$
25	24	excomimw	$⊢ \exists y \exists x (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
26	17 25	sylbir	$⊢ \exists y (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w) \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
27	12 26	syl	$⊢ A \in V \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$

Metamath Proof Explorer

Theorem cflem

Proof