Theorem iotanul2

Description: Version of iotanul using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

	Ref	Expression
Assertion	iotanul2	$$⊢\neg \exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-iota	$$⊢\left(\iota x|\phi \right)=\bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}$$
2		n0	$$⊢\bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\ne \varnothing \leftrightarrow \exists vv\in \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}$$
3		eluni	$$⊢v\in \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\leftrightarrow \exists y\left(v\in y\wedge y\in \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\right)$$
4		vex	$$⊢y\in \mathrm{V}$$
5		sneq	$$⊢w=y\to \left\{w\right\}=\left\{y\right\}$$
6	5	eqeq2d	$$⊢w=y\to \left(\left\{x|\phi \right\}=\left\{w\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{y\right\}\right)$$
7	4 6	elab	$$⊢y\in \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\leftrightarrow \left\{x|\phi \right\}=\left\{y\right\}$$
8	7	biimpi	$$⊢y\in \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\to \left\{x|\phi \right\}=\left\{y\right\}$$
9	8	adantl	$$⊢\left(v\in y\wedge y\in \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\right)\to \left\{x|\phi \right\}=\left\{y\right\}$$
10	9	eximi	$$⊢\exists y\left(v\in y\wedge y\in \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\right)\to \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
11	3 10	sylbi	$$⊢v\in \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\to \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
12	11	exlimiv	$$⊢\exists vv\in \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\to \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
13	2 12	sylbi	$$⊢\bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}\ne \varnothing \to \exists y\left\{x|\phi \right\}=\left\{y\right\}$$
14	13	necon1bi	$$⊢\neg \exists y\left\{x|\phi \right\}=\left\{y\right\}\to \bigcup \left\{w|\left\{x|\phi \right\}=\left\{w\right\}\right\}=\varnothing$$
15	1 14	eqtrid	$$⊢\neg \exists y\left\{x|\phi \right\}=\left\{y\right\}\to \left(\iota x|\phi \right)=\varnothing$$