Theorem tcsni

Description: The transitive closure of a singleton. Proof suggested by Gérard Lang. (Contributed by Mario Carneiro, 4-Jun-2015)

	Ref	Expression
Hypothesis	tc2.1	$$⊢A\in \mathrm{V}$$
Assertion	tcsni	$$⊢\mathrm{TC}\left(\left\{A\right\}\right)=\mathrm{TC}\left(A\right)\cup \left\{A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		tc2.1	$$⊢A\in \mathrm{V}$$
2	1	snss	$$⊢A\in x\leftrightarrow \left\{A\right\}\subseteq x$$
3	2	anbi1i	$$⊢\left(A\in x\wedge \mathrm{Tr}x\right)\leftrightarrow \left(\left\{A\right\}\subseteq x\wedge \mathrm{Tr}x\right)$$
4	3	abbii	$$⊢\left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}=\left\{x|\left(\left\{A\right\}\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
5	4	inteqi	$$⊢\bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}=\bigcap \left\{x|\left(\left\{A\right\}\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
6	1	tc2	$$⊢\mathrm{TC}\left(A\right)\cup \left\{A\right\}=\bigcap \left\{x|\left(A\in x\wedge \mathrm{Tr}x\right)\right\}$$
7		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
8		tcvalg	$$⊢\left\{A\right\}\in \mathrm{V}\to \mathrm{TC}\left(\left\{A\right\}\right)=\bigcap \left\{x|\left(\left\{A\right\}\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
9	7 8	ax-mp	$$⊢\mathrm{TC}\left(\left\{A\right\}\right)=\bigcap \left\{x|\left(\left\{A\right\}\subseteq x\wedge \mathrm{Tr}x\right)\right\}$$
10	5 6 9	3eqtr4ri	$$⊢\mathrm{TC}\left(\left\{A\right\}\right)=\mathrm{TC}\left(A\right)\cup \left\{A\right\}$$