Metamath Proof Explorer

Theorem inf2

Description: Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf as a hypothesis). Abbreviated version of the Axiom of Infinity in FreydScedrov p. 283. (Contributed by NM, 28-Oct-1996)

		Ref	Expression
	Hypothesis	inf1.1	$⊢ \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
	Assertion	inf2	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x)$

Proof

Step	Hyp	Ref	Expression
1		inf1.1	$⊢ \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
2	1	inf1	$⊢ \exists x (x \neq \emptyset \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
3		df-ss	$⊢ x \subseteq ⋃ x \leftrightarrow \forall y (y \in x \to y \in ⋃ x)$
4		eluni	$⊢ y \in ⋃ x \leftrightarrow \exists z (y \in z \land z \in x)$
5	4	imbi2i	$⊢ (y \in x \to y \in ⋃ x) \leftrightarrow (y \in x \to \exists z (y \in z \land z \in x))$
6	5	albii	$⊢ \forall y (y \in x \to y \in ⋃ x) \leftrightarrow \forall y (y \in x \to \exists z (y \in z \land z \in x))$
7	3 6	bitri	$⊢ x \subseteq ⋃ x \leftrightarrow \forall y (y \in x \to \exists z (y \in z \land z \in x))$
8	7	anbi2i	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow (x \neq \emptyset \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
9	8	exbii	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x) \leftrightarrow \exists x (x \neq \emptyset \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
10	2 9	mpbir	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x)$