iotanul2

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

		Ref	Expression
	Assertion	iotanul2	$⊢ \neg \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = \emptyset$

Step	Hyp	Ref	Expression
1		df-iota	$⊢ (ι x \| φ) = ⋃ \{w \| \{x \| φ\} = \{w\}\}$
2		n0	$⊢ ⋃ \{w \| \{x \| φ\} = \{w\}\} \neq \emptyset \leftrightarrow \exists v v \in ⋃ \{w \| \{x \| φ\} = \{w\}\}$
3		eluni	$⊢ v \in ⋃ \{w \| \{x \| φ\} = \{w\}\} \leftrightarrow \exists y (v \in y \land y \in \{w \| \{x \| φ\} = \{w\}\})$
4		vex	$⊢ y \in V$
5		sneq	$⊢ w = y \to \{w\} = \{y\}$
6	5	eqeq2d	$⊢ w = y \to (\{x \| φ\} = \{w\} \leftrightarrow \{x \| φ\} = \{y\})$
7	4 6	elab	$⊢ y \in \{w \| \{x \| φ\} = \{w\}\} \leftrightarrow \{x \| φ\} = \{y\}$
8	7	biimpi	$⊢ y \in \{w \| \{x \| φ\} = \{w\}\} \to \{x \| φ\} = \{y\}$
9	8	adantl	$⊢ (v \in y \land y \in \{w \| \{x \| φ\} = \{w\}\}) \to \{x \| φ\} = \{y\}$
10	9	eximi	$⊢ \exists y (v \in y \land y \in \{w \| \{x \| φ\} = \{w\}\}) \to \exists y \{x \| φ\} = \{y\}$
11	3 10	sylbi	$⊢ v \in ⋃ \{w \| \{x \| φ\} = \{w\}\} \to \exists y \{x \| φ\} = \{y\}$
12	11	exlimiv	$⊢ \exists v v \in ⋃ \{w \| \{x \| φ\} = \{w\}\} \to \exists y \{x \| φ\} = \{y\}$
13	2 12	sylbi	$⊢ ⋃ \{w \| \{x \| φ\} = \{w\}\} \neq \emptyset \to \exists y \{x \| φ\} = \{y\}$
14	13	necon1bi	$⊢ \neg \exists y \{x \| φ\} = \{y\} \to ⋃ \{w \| \{x \| φ\} = \{w\}\} = \emptyset$
15	1 14	eqtrid	$⊢ \neg \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = \emptyset$

Metamath Proof Explorer