infeq5

Description: The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex .) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	infeq5	$⊢ \exists x x \subset ⋃ x \leftrightarrow ω \in V$

Proof

Step	Hyp	Ref	Expression
1		df-pss	$⊢ x \subset ⋃ x \leftrightarrow (x \subseteq ⋃ x \land x \neq ⋃ x)$
2		unieq	$⊢ x = \emptyset \to ⋃ x = ⋃ \emptyset$
3		uni0	$⊢ ⋃ \emptyset = \emptyset$
4	2 3	eqtr2di	$⊢ x = \emptyset \to \emptyset = ⋃ x$
5		eqtr	$⊢ (x = \emptyset \land \emptyset = ⋃ x) \to x = ⋃ x$
6	4 5	mpdan	$⊢ x = \emptyset \to x = ⋃ x$
7	6	necon3i	$⊢ x \neq ⋃ x \to x \neq \emptyset$
8	7	anim1i	$⊢ (x \neq ⋃ x \land x \subseteq ⋃ x) \to (x \neq \emptyset \land x \subseteq ⋃ x)$
9	8	ancoms	$⊢ (x \subseteq ⋃ x \land x \neq ⋃ x) \to (x \neq \emptyset \land x \subseteq ⋃ x)$
10	1 9	sylbi	$⊢ x \subset ⋃ x \to (x \neq \emptyset \land x \subseteq ⋃ x)$
11	10	eximi	$⊢ \exists x x \subset ⋃ x \to \exists x (x \neq \emptyset \land x \subseteq ⋃ x)$
12		eqid	$⊢ (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\}) = (y \in V ⟼ \{w \in x \| w \cap x \subseteq y\})$
13		eqid	$⊢ {rec ((y \in V ⟼ \{w \in x \| w \cap x \subseteq y\}), \emptyset) ↾}_{ω} = {rec ((y \in V ⟼ \{w \in x \| w \cap x \subseteq y\}), \emptyset) ↾}_{ω}$
14		vex	$⊢ x \in V$
15	12 13 14 14	inf3lem7	$⊢ (x \neq \emptyset \land x \subseteq ⋃ x) \to ω \in V$
16	15	exlimiv	$⊢ \exists x (x \neq \emptyset \land x \subseteq ⋃ x) \to ω \in V$
17	11 16	syl	$⊢ \exists x x \subset ⋃ x \to ω \in V$
18		infeq5i	$⊢ ω \in V \to \exists x x \subset ⋃ x$
19	17 18	impbii	$⊢ \exists x x \subset ⋃ x \leftrightarrow ω \in V$

Metamath Proof Explorer

Theorem infeq5

Proof