Theorem trintss

Description: Any nonempty transitive class includes its intersection. Exercise 3 in TakeutiZaring p. 44 (which mistakenly does not include the nonemptiness hypothesis). (Contributed by Scott Fenton, 3-Mar-2011) (Proof shortened by Andrew Salmon, 14-Nov-2011)

	Ref	Expression
Assertion	trintss	$$⊢\left(\mathrm{Tr}A\wedge A\ne \varnothing \right)\to \bigcap A\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		intss1	$$⊢x\in A\to \bigcap A\subseteq x$$
3		trss	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\subseteq A\right)$$
4	3	com12	$$⊢x\in A\to \left(\mathrm{Tr}A\to x\subseteq A\right)$$
5		sstr2	$$⊢\bigcap A\subseteq x\to \left(x\subseteq A\to \bigcap A\subseteq A\right)$$
6	2 4 5	sylsyld	$$⊢x\in A\to \left(\mathrm{Tr}A\to \bigcap A\subseteq A\right)$$
7	6	exlimiv	$$⊢\exists xx\in A\to \left(\mathrm{Tr}A\to \bigcap A\subseteq A\right)$$
8	1 7	sylbi	$$⊢A\ne \varnothing \to \left(\mathrm{Tr}A\to \bigcap A\subseteq A\right)$$
9	8	impcom	$$⊢\left(\mathrm{Tr}A\wedge A\ne \varnothing \right)\to \bigcap A\subseteq A$$