Theorem 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 xx\subset \bigcup x\leftrightarrow \mathrm{\omega }\in \mathrm{V}$$

Proof

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