dfiota3

Description: A definition of iota using minimal quantifiers. (Contributed by Scott Fenton, 19-Feb-2013)

		Ref	Expression
	Assertion	dfiota3	$⊢ (ι x \| φ) = ⋃ ⋃ (\{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$

Proof

Step	Hyp	Ref	Expression
1		df-iota	$⊢ (ι x \| φ) = ⋃ \{y \| \{x \| φ\} = \{y\}\}$
2		abeq1	$⊢ \{y \| \{x \| φ\} = \{y\}\} = ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\} \leftrightarrow \forall y (\{x \| φ\} = \{y\} \leftrightarrow y \in ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\})$
3		exdistr	$⊢ \exists z \exists w (y \in z \land (z = \{x \| φ\} \land z = \{w\})) \leftrightarrow \exists z (y \in z \land \exists w (z = \{x \| φ\} \land z = \{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	ceqsexv	$⊢ \exists w (w = y \land \{x \| φ\} = \{w\}) \leftrightarrow \{x \| φ\} = \{y\}$
8		snex	$⊢ \{w\} \in V$
9		eqeq1	$⊢ z = \{w\} \to (z = \{x \| φ\} \leftrightarrow \{w\} = \{x \| φ\})$
10		eleq2	$⊢ z = \{w\} \to (y \in z \leftrightarrow y \in \{w\})$
11	9 10	anbi12d	$⊢ z = \{w\} \to ((z = \{x \| φ\} \land y \in z) \leftrightarrow (\{w\} = \{x \| φ\} \land y \in \{w\}))$
12		eqcom	$⊢ \{w\} = \{x \| φ\} \leftrightarrow \{x \| φ\} = \{w\}$
13		velsn	$⊢ y \in \{w\} \leftrightarrow y = w$
14		equcom	$⊢ y = w \leftrightarrow w = y$
15	13 14	bitri	$⊢ y \in \{w\} \leftrightarrow w = y$
16	12 15	anbi12ci	$⊢ (\{w\} = \{x \| φ\} \land y \in \{w\}) \leftrightarrow (w = y \land \{x \| φ\} = \{w\})$
17	11 16	syl6bb	$⊢ z = \{w\} \to ((z = \{x \| φ\} \land y \in z) \leftrightarrow (w = y \land \{x \| φ\} = \{w\}))$
18	8 17	ceqsexv	$⊢ \exists z (z = \{w\} \land (z = \{x \| φ\} \land y \in z)) \leftrightarrow (w = y \land \{x \| φ\} = \{w\})$
19		an13	$⊢ (z = \{w\} \land (z = \{x \| φ\} \land y \in z)) \leftrightarrow (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
20	19	exbii	$⊢ \exists z (z = \{w\} \land (z = \{x \| φ\} \land y \in z)) \leftrightarrow \exists z (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
21	18 20	bitr3i	$⊢ (w = y \land \{x \| φ\} = \{w\}) \leftrightarrow \exists z (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
22	21	exbii	$⊢ \exists w (w = y \land \{x \| φ\} = \{w\}) \leftrightarrow \exists w \exists z (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
23	7 22	bitr3i	$⊢ \{x \| φ\} = \{y\} \leftrightarrow \exists w \exists z (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
24		excom	$⊢ \exists w \exists z (y \in z \land (z = \{x \| φ\} \land z = \{w\})) \leftrightarrow \exists z \exists w (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
25	23 24	bitri	$⊢ \{x \| φ\} = \{y\} \leftrightarrow \exists z \exists w (y \in z \land (z = \{x \| φ\} \land z = \{w\}))$
26		eluniab	$⊢ y \in ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\} \leftrightarrow \exists z (y \in z \land \exists w (z = \{x \| φ\} \land z = \{w\}))$
27	3 25 26	3bitr4i	$⊢ \{x \| φ\} = \{y\} \leftrightarrow y \in ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
28	2 27	mpgbir	$⊢ \{y \| \{x \| φ\} = \{y\}\} = ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
29		df-sn	$⊢ \{\{x \| φ\}\} = \{z \| z = \{x \| φ\}\}$
30		dfsingles2	$⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = \{z \| \exists w z = \{w\}\}$
31	29 30	ineq12i	$⊢ \{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = \{z \| z = \{x \| φ\}\} \cap \{z \| \exists w z = \{w\}\}$
32		inab	$⊢ \{z \| z = \{x \| φ\}\} \cap \{z \| \exists w z = \{w\}\} = \{z \| (z = \{x \| φ\} \land \exists w z = \{w\})\}$
33		19.42v	$⊢ \exists w (z = \{x \| φ\} \land z = \{w\}) \leftrightarrow (z = \{x \| φ\} \land \exists w z = \{w\})$
34	33	bicomi	$⊢ (z = \{x \| φ\} \land \exists w z = \{w\}) \leftrightarrow \exists w (z = \{x \| φ\} \land z = \{w\})$
35	34	abbii	$⊢ \{z \| (z = \{x \| φ\} \land \exists w z = \{w\})\} = \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
36	32 35	eqtri	$⊢ \{z \| z = \{x \| φ\}\} \cap \{z \| \exists w z = \{w\}\} = \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
37	31 36	eqtri	$⊢ \{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 = \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
38	37	unieqi	$⊢ ⋃ (\{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌) = ⋃ \{z \| \exists w (z = \{x \| φ\} \land z = \{w\})\}$
39	28 38	eqtr4i	$⊢ \{y \| \{x \| φ\} = \{y\}\} = ⋃ (\{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
40	39	unieqi	$⊢ ⋃ \{y \| \{x \| φ\} = \{y\}\} = ⋃ ⋃ (\{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$
41	1 40	eqtri	$⊢ (ι x \| φ) = ⋃ ⋃ (\{\{x \| φ\}\} \cap 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌)$

Metamath Proof Explorer

Theorem dfiota3

Proof