This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inf5

Description: The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (see Theorem infeq5 ). This provides us with a very compact way to express the Axiom of Infinity using only elementary symbols. (Contributed by NM, 3-Jun-2005)

		Ref	Expression
	Assertion	inf5	⊢ ∃ 𝑥 𝑥 ⊊ ∪ 𝑥

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		infeq5i	⊢ ( ω ∈ V → ∃ 𝑥 𝑥 ⊊ ∪ 𝑥 )
3	1 2	ax-mp	⊢ ∃ 𝑥 𝑥 ⊊ ∪ 𝑥