Theorem itunitc

Description: The union of all union iterates creates the transitive closure; compare trcl . (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	itunitc	$$⊢\mathrm{TC}\left(A\right)=\bigcup \mathrm{ran}U\left(A\right)$$

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		fveq2	$$⊢a=A\to \mathrm{TC}\left(a\right)=\mathrm{TC}\left(A\right)$$
3		fveq2	$$⊢a=A\to U\left(a\right)=U\left(A\right)$$
4	3	rneqd	$$⊢a=A\to \mathrm{ran}U\left(a\right)=\mathrm{ran}U\left(A\right)$$
5	4	unieqd	$$⊢a=A\to \bigcup \mathrm{ran}U\left(a\right)=\bigcup \mathrm{ran}U\left(A\right)$$
6	2 5	eqeq12d	$$⊢a=A\to \left(\mathrm{TC}\left(a\right)=\bigcup \mathrm{ran}U\left(a\right)\leftrightarrow \mathrm{TC}\left(A\right)=\bigcup \mathrm{ran}U\left(A\right)\right)$$
7	1	ituni0	$$⊢a\in \mathrm{V}\to U\left(a\right)\left(\varnothing \right)=a$$
8	7	elv	$$⊢U\left(a\right)\left(\varnothing \right)=a$$
9		fvssunirn	$$⊢U\left(a\right)\left(\varnothing \right)\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
10	8 9	eqsstrri	$$⊢a\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
11		dftr3	$$⊢\mathrm{Tr}\bigcup \mathrm{ran}U\left(a\right)\leftrightarrow \forall b\in \bigcup \mathrm{ran}U\left(a\right)b\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
12		vex	$$⊢a\in \mathrm{V}$$
13	1	itunifn	$$⊢a\in \mathrm{V}\to U\left(a\right)Fn\mathrm{\omega }$$
14		fnunirn	$$⊢U\left(a\right)Fn\mathrm{\omega }\to \left(b\in \bigcup \mathrm{ran}U\left(a\right)\leftrightarrow \exists c\in \mathrm{\omega }b\in U\left(a\right)\left(c\right)\right)$$
15	12 13 14	mp2b	$$⊢b\in \bigcup \mathrm{ran}U\left(a\right)\leftrightarrow \exists c\in \mathrm{\omega }b\in U\left(a\right)\left(c\right)$$
16		elssuni	$$⊢b\in U\left(a\right)\left(c\right)\to b\subseteq \bigcup U\left(a\right)\left(c\right)$$
17	1	itunisuc	$$⊢U\left(a\right)\left(\mathrm{suc}c\right)=\bigcup U\left(a\right)\left(c\right)$$
18		fvssunirn	$$⊢U\left(a\right)\left(\mathrm{suc}c\right)\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
19	17 18	eqsstrri	$$⊢\bigcup U\left(a\right)\left(c\right)\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
20	16 19	sstrdi	$$⊢b\in U\left(a\right)\left(c\right)\to b\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
21	20	rexlimivw	$$⊢\exists c\in \mathrm{\omega }b\in U\left(a\right)\left(c\right)\to b\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
22	15 21	sylbi	$$⊢b\in \bigcup \mathrm{ran}U\left(a\right)\to b\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
23	11 22	mprgbir	$$⊢\mathrm{Tr}\bigcup \mathrm{ran}U\left(a\right)$$
24		tcmin	$$⊢a\in \mathrm{V}\to \left(\left(a\subseteq \bigcup \mathrm{ran}U\left(a\right)\wedge \mathrm{Tr}\bigcup \mathrm{ran}U\left(a\right)\right)\to \mathrm{TC}\left(a\right)\subseteq \bigcup \mathrm{ran}U\left(a\right)\right)$$
25	24	elv	$$⊢\left(a\subseteq \bigcup \mathrm{ran}U\left(a\right)\wedge \mathrm{Tr}\bigcup \mathrm{ran}U\left(a\right)\right)\to \mathrm{TC}\left(a\right)\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
26	10 23 25	mp2an	$$⊢\mathrm{TC}\left(a\right)\subseteq \bigcup \mathrm{ran}U\left(a\right)$$
27		unissb	$$⊢\bigcup \mathrm{ran}U\left(a\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow \forall b\in \mathrm{ran}U\left(a\right)b\subseteq \mathrm{TC}\left(a\right)$$
28		fvelrnb	$$⊢U\left(a\right)Fn\mathrm{\omega }\to \left(b\in \mathrm{ran}U\left(a\right)\leftrightarrow \exists c\in \mathrm{\omega }U\left(a\right)\left(c\right)=b\right)$$
29	12 13 28	mp2b	$$⊢b\in \mathrm{ran}U\left(a\right)\leftrightarrow \exists c\in \mathrm{\omega }U\left(a\right)\left(c\right)=b$$
30	1	itunitc1	$$⊢U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)$$
31	30	a1i	$$⊢c\in \mathrm{\omega }\to U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)$$
32		sseq1	$$⊢U\left(a\right)\left(c\right)=b\to \left(U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow b\subseteq \mathrm{TC}\left(a\right)\right)$$
33	31 32	syl5ibcom	$$⊢c\in \mathrm{\omega }\to \left(U\left(a\right)\left(c\right)=b\to b\subseteq \mathrm{TC}\left(a\right)\right)$$
34	33	rexlimiv	$$⊢\exists c\in \mathrm{\omega }U\left(a\right)\left(c\right)=b\to b\subseteq \mathrm{TC}\left(a\right)$$
35	29 34	sylbi	$$⊢b\in \mathrm{ran}U\left(a\right)\to b\subseteq \mathrm{TC}\left(a\right)$$
36	27 35	mprgbir	$$⊢\bigcup \mathrm{ran}U\left(a\right)\subseteq \mathrm{TC}\left(a\right)$$
37	26 36	eqssi	$$⊢\mathrm{TC}\left(a\right)=\bigcup \mathrm{ran}U\left(a\right)$$
38	6 37	vtoclg	$$⊢A\in \mathrm{V}\to \mathrm{TC}\left(A\right)=\bigcup \mathrm{ran}U\left(A\right)$$
39		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
40	39	unieqi	$$⊢\bigcup \mathrm{ran}\varnothing =\bigcup \varnothing$$
41		uni0	$$⊢\bigcup \varnothing =\varnothing$$
42	40 41	eqtr2i	$$⊢\varnothing =\bigcup \mathrm{ran}\varnothing$$
43		fvprc	$$⊢\neg A\in \mathrm{V}\to \mathrm{TC}\left(A\right)=\varnothing$$
44		fvprc	$$⊢\neg A\in \mathrm{V}\to U\left(A\right)=\varnothing$$
45	44	rneqd	$$⊢\neg A\in \mathrm{V}\to \mathrm{ran}U\left(A\right)=\mathrm{ran}\varnothing$$
46	45	unieqd	$$⊢\neg A\in \mathrm{V}\to \bigcup \mathrm{ran}U\left(A\right)=\bigcup \mathrm{ran}\varnothing$$
47	42 43 46	3eqtr4a	$$⊢\neg A\in \mathrm{V}\to \mathrm{TC}\left(A\right)=\bigcup \mathrm{ran}U\left(A\right)$$
48	38 47	pm2.61i	$$⊢\mathrm{TC}\left(A\right)=\bigcup \mathrm{ran}U\left(A\right)$$