Theorem itunitc1

Description: Each union iterate is a member of the transitive closure. (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	itunitc1	$$⊢U\left(A\right)\left(B\right)\subseteq \mathrm{TC}\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 U\left(a\right)=U\left(A\right)$$
3	2	fveq1d	$$⊢a=A\to U\left(a\right)\left(B\right)=U\left(A\right)\left(B\right)$$
4		fveq2	$$⊢a=A\to \mathrm{TC}\left(a\right)=\mathrm{TC}\left(A\right)$$
5	3 4	sseq12d	$$⊢a=A\to \left(U\left(a\right)\left(B\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow U\left(A\right)\left(B\right)\subseteq \mathrm{TC}\left(A\right)\right)$$
6		fveq2	$$⊢b=\varnothing \to U\left(a\right)\left(b\right)=U\left(a\right)\left(\varnothing \right)$$
7	6	sseq1d	$$⊢b=\varnothing \to \left(U\left(a\right)\left(b\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow U\left(a\right)\left(\varnothing \right)\subseteq \mathrm{TC}\left(a\right)\right)$$
8		fveq2	$$⊢b=c\to U\left(a\right)\left(b\right)=U\left(a\right)\left(c\right)$$
9	8	sseq1d	$$⊢b=c\to \left(U\left(a\right)\left(b\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)\right)$$
10		fveq2	$$⊢b=\mathrm{suc}c\to U\left(a\right)\left(b\right)=U\left(a\right)\left(\mathrm{suc}c\right)$$
11	10	sseq1d	$$⊢b=\mathrm{suc}c\to \left(U\left(a\right)\left(b\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow U\left(a\right)\left(\mathrm{suc}c\right)\subseteq \mathrm{TC}\left(a\right)\right)$$
12		fveq2	$$⊢b=B\to U\left(a\right)\left(b\right)=U\left(a\right)\left(B\right)$$
13	12	sseq1d	$$⊢b=B\to \left(U\left(a\right)\left(b\right)\subseteq \mathrm{TC}\left(a\right)\leftrightarrow U\left(a\right)\left(B\right)\subseteq \mathrm{TC}\left(a\right)\right)$$
14	1	ituni0	$$⊢a\in \mathrm{V}\to U\left(a\right)\left(\varnothing \right)=a$$
15		tcid	$$⊢a\in \mathrm{V}\to a\subseteq \mathrm{TC}\left(a\right)$$
16	14 15	eqsstrd	$$⊢a\in \mathrm{V}\to U\left(a\right)\left(\varnothing \right)\subseteq \mathrm{TC}\left(a\right)$$
17	16	elv	$$⊢U\left(a\right)\left(\varnothing \right)\subseteq \mathrm{TC}\left(a\right)$$
18	1	itunisuc	$$⊢U\left(a\right)\left(\mathrm{suc}c\right)=\bigcup U\left(a\right)\left(c\right)$$
19		tctr	$$⊢\mathrm{Tr}\mathrm{TC}\left(a\right)$$
20		pwtr	$$⊢\mathrm{Tr}\mathrm{TC}\left(a\right)\leftrightarrow \mathrm{Tr}𝒫\mathrm{TC}\left(a\right)$$
21	19 20	mpbi	$$⊢\mathrm{Tr}𝒫\mathrm{TC}\left(a\right)$$
22		trss	$$⊢\mathrm{Tr}𝒫\mathrm{TC}\left(a\right)\to \left(U\left(a\right)\left(c\right)\in 𝒫\mathrm{TC}\left(a\right)\to U\left(a\right)\left(c\right)\subseteq 𝒫\mathrm{TC}\left(a\right)\right)$$
23	21 22	ax-mp	$$⊢U\left(a\right)\left(c\right)\in 𝒫\mathrm{TC}\left(a\right)\to U\left(a\right)\left(c\right)\subseteq 𝒫\mathrm{TC}\left(a\right)$$
24		fvex	$$⊢U\left(a\right)\left(c\right)\in \mathrm{V}$$
25	24	elpw	$$⊢U\left(a\right)\left(c\right)\in 𝒫\mathrm{TC}\left(a\right)\leftrightarrow U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)$$
26		sspwuni	$$⊢U\left(a\right)\left(c\right)\subseteq 𝒫\mathrm{TC}\left(a\right)\leftrightarrow \bigcup U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)$$
27	23 25 26	3imtr3i	$$⊢U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)\to \bigcup U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)$$
28	18 27	eqsstrid	$$⊢U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)\to U\left(a\right)\left(\mathrm{suc}c\right)\subseteq \mathrm{TC}\left(a\right)$$
29	28	a1i	$$⊢c\in \mathrm{\omega }\to \left(U\left(a\right)\left(c\right)\subseteq \mathrm{TC}\left(a\right)\to U\left(a\right)\left(\mathrm{suc}c\right)\subseteq \mathrm{TC}\left(a\right)\right)$$
30	7 9 11 13 17 29	finds	$$⊢B\in \mathrm{\omega }\to U\left(a\right)\left(B\right)\subseteq \mathrm{TC}\left(a\right)$$
31		vex	$$⊢a\in \mathrm{V}$$
32	1	itunifn	$$⊢a\in \mathrm{V}\to U\left(a\right)Fn\mathrm{\omega }$$
33		fndm	$$⊢U\left(a\right)Fn\mathrm{\omega }\to \mathrm{dom}U\left(a\right)=\mathrm{\omega }$$
34	31 32 33	mp2b	$$⊢\mathrm{dom}U\left(a\right)=\mathrm{\omega }$$
35	34	eleq2i	$$⊢B\in \mathrm{dom}U\left(a\right)\leftrightarrow B\in \mathrm{\omega }$$
36		ndmfv	$$⊢\neg B\in \mathrm{dom}U\left(a\right)\to U\left(a\right)\left(B\right)=\varnothing$$
37	35 36	sylnbir	$$⊢\neg B\in \mathrm{\omega }\to U\left(a\right)\left(B\right)=\varnothing$$
38		0ss	$$⊢\varnothing \subseteq \mathrm{TC}\left(a\right)$$
39	37 38	eqsstrdi	$$⊢\neg B\in \mathrm{\omega }\to U\left(a\right)\left(B\right)\subseteq \mathrm{TC}\left(a\right)$$
40	30 39	pm2.61i	$$⊢U\left(a\right)\left(B\right)\subseteq \mathrm{TC}\left(a\right)$$
41	5 40	vtoclg	$$⊢A\in \mathrm{V}\to U\left(A\right)\left(B\right)\subseteq \mathrm{TC}\left(A\right)$$
42		fv2prc	$$⊢\neg A\in \mathrm{V}\to U\left(A\right)\left(B\right)=\varnothing$$
43		0ss	$$⊢\varnothing \subseteq \mathrm{TC}\left(A\right)$$
44	42 43	eqsstrdi	$$⊢\neg A\in \mathrm{V}\to U\left(A\right)\left(B\right)\subseteq \mathrm{TC}\left(A\right)$$
45	41 44	pm2.61i	$$⊢U\left(A\right)\left(B\right)\subseteq \mathrm{TC}\left(A\right)$$