Theorem itunifn

Description: Functionality of the iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Hypothesis	ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
Assertion	itunifn	$$⊢A\in V\to U\left(A\right)Fn\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ituni.u	$$⊢U=\left(x\in \mathrm{V}⟼{\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),x\right)\upharpoonright }_{\mathrm{\omega }}\right)$$
2		frfnom	$$⊢\left({\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }$$
3	1	itunifval	$$⊢A\in V\to U\left(A\right)={\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}$$
4	3	fneq1d	$$⊢A\in V\to \left(U\left(A\right)Fn\mathrm{\omega }\leftrightarrow \left({\mathrm{rec}\left(\left(y\in \mathrm{V}⟼\bigcup y\right),A\right)\upharpoonright }_{\mathrm{\omega }}\right)Fn\mathrm{\omega }\right)$$
5	2 4	mpbiri	$$⊢A\in V\to U\left(A\right)Fn\mathrm{\omega }$$