Theorem tc2

Description: A variant of the definition of the transitive closure function, using instead the smallest transitive set containing A as a member, gives almost the same set, except that A itself must be added because it is not usually a member of ( TCA ) (and it is never a member if A is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013)

	Ref	Expression
Hypothesis	tc2.1	$$⊢A\in \mathrm{V}$$
Assertion	tc2	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}=\bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		tc2.1	$$⊢A\in \mathrm{V}$$
2		tcvalg	$$⊢A\in \mathrm{V}\to \mathrm{TC}\left(A\right)=\bigcap \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
3	1 2	ax-mp	$$⊢\mathrm{TC}\left(A\right)=\bigcap \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
4		trss	$$⊢\mathrm{Tr}x\to \left(A\in x\to A\subseteq x\right)$$
5	4	imdistanri	$$⊢\left(A\in x\wedge \mathrm{Tr}x\right)\to \left(A\subseteq x\wedge \mathrm{Tr}x\right)$$
6	5	ss2abi	$$⊢\left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\subseteq \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
7		intss	$$⊢\left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\subseteq \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}\to \bigcap \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
8	6 7	ax-mp	$$⊢\bigcap \left\{x|\left(A\subseteq x\wedge \mathrm{Tr}x\right)\right\}\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
9	3 8	eqsstri	$$⊢\mathrm{TC}\left(A\right)\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
10	1	elintab	$$⊢A\in \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\leftrightarrow \forall x\left(\left(A\in x\wedge \mathrm{Tr}x\right)\to A\in x\right)$$
11		simpl	$$⊢\left(A\in x\wedge \mathrm{Tr}x\right)\to A\in x$$
12	10 11	mpgbir	$$⊢A\in \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
13	1	snss	$$⊢A\in \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\leftrightarrow \left\{A\right\}\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
14	12 13	mpbi	$$⊢\left\{A\right\}\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
15	9 14	unssi	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}\subseteq \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
16	1	snid	$$⊢A\in \left\{A\right\}$$
17		elun2	$$⊢A\in \left\{A\right\}\to A\in \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)$$
18	16 17	ax-mp	$$⊢A\in \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)$$
19		uniun	$$⊢\bigcup \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)=\bigcup \mathrm{TC}\left(A\right)\cup \bigcup \left\{A\right\}$$
20		tctr	$$⊢\mathrm{Tr}\mathrm{TC}\left(A\right)$$
21		df-tr	$$⊢\mathrm{Tr}\mathrm{TC}\left(A\right)\leftrightarrow \bigcup \mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)$$
22	20 21	mpbi	$$⊢\bigcup \mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)$$
23	1	unisn	$$⊢\bigcup \left\{A\right\}=A$$
24		tcid	$$⊢A\in \mathrm{V}\to A\subseteq \mathrm{TC}\left(A\right)$$
25	1 24	ax-mp	$$⊢A\subseteq \mathrm{TC}\left(A\right)$$
26	23 25	eqsstri	$$⊢\bigcup \left\{A\right\}\subseteq \mathrm{TC}\left(A\right)$$
27	22 26	unssi	$$⊢\bigcup \mathrm{TC}\left(A\right)\cup \bigcup \left\{A\right\}\subseteq \mathrm{TC}\left(A\right)$$
28	19 27	eqsstri	$$⊢\bigcup \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\subseteq \mathrm{TC}\left(A\right)$$
29		ssun1	$$⊢\mathrm{TC}\left(A\right)\subseteq \mathrm{TC}\left(A\right)\cup \left\{A\right\}$$
30	28 29	sstri	$$⊢\bigcup \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\subseteq \mathrm{TC}\left(A\right)\cup \left\{A\right\}$$
31		df-tr	$$⊢\mathrm{Tr}\left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\leftrightarrow \bigcup \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\subseteq \mathrm{TC}\left(A\right)\cup \left\{A\right\}$$
32	30 31	mpbir	$$⊢\mathrm{Tr}\left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)$$
33		fvex	$$⊢\mathrm{TC}\left(A\right)\in \mathrm{V}$$
34		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
35	33 34	unex	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}\in \mathrm{V}$$
36		eleq2	$$⊢x=\mathrm{TC}\left(A\right)\cup \left\{A\right\}\to \left(A\in x\leftrightarrow A\in \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\right)$$
37		treq	$$⊢x=\mathrm{TC}\left(A\right)\cup \left\{A\right\}\to \left(\mathrm{Tr}x\leftrightarrow \mathrm{Tr}\left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\right)$$
38	36 37	anbi12d	$$⊢x=\mathrm{TC}\left(A\right)\cup \left\{A\right\}\to \left(\left(A\in x\wedge \mathrm{Tr}x\right)\leftrightarrow \left(A\in \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\wedge \mathrm{Tr}\left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\right)\right)$$
39	35 38	elab	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}\in \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\leftrightarrow \left(A\in \left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\wedge \mathrm{Tr}\left(\mathrm{TC}\left(A\right)\cup \left\{A\right\}\right)\right)$$
40	18 32 39	mpbir2an	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}\in \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
41		intss1	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}\in \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\to \bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\subseteq \mathrm{TC}\left(A\right)\cup \left\{A\right\}$$
42	40 41	ax-mp	$$⊢\bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}\subseteq \mathrm{TC}\left(A\right)\cup \left\{A\right\}$$
43	15 42	eqssi	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}=\bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$