Theorem trficl

Description: The class of all transitive relations has the finite intersection property. (Contributed by RP, 1-Jan-2020) (Proof shortened by RP, 3-Jan-2020)

	Ref	Expression
Hypothesis	trficl.a	$$⊢A=\left\{z|z\circ z\subseteq z\right\}$$
Assertion	trficl	$$⊢\forall x\in A\forall y\in Ax\cap y\in A$$

Proof

Step	Hyp	Ref	Expression
1		trficl.a	$$⊢A=\left\{z|z\circ z\subseteq z\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	inex1	$$⊢x\cap y\in \mathrm{V}$$
4		id	$$⊢z=x\cap y\to z=x\cap y$$
5	4 4	coeq12d	$$⊢z=x\cap y\to z\circ z=\left(x\cap y\right)\circ \left(x\cap y\right)$$
6	5 4	sseq12d	$$⊢z=x\cap y\to \left(z\circ z\subseteq z\leftrightarrow \left(x\cap y\right)\circ \left(x\cap y\right)\subseteq x\cap y\right)$$
7		id	$$⊢z=x\to z=x$$
8	7 7	coeq12d	$$⊢z=x\to z\circ z=x\circ x$$
9	8 7	sseq12d	$$⊢z=x\to \left(z\circ z\subseteq z\leftrightarrow x\circ x\subseteq x\right)$$
10		id	$$⊢z=y\to z=y$$
11	10 10	coeq12d	$$⊢z=y\to z\circ z=y\circ y$$
12	11 10	sseq12d	$$⊢z=y\to \left(z\circ z\subseteq z\leftrightarrow y\circ y\subseteq y\right)$$
13		trin2	$$⊢\left(x\circ x\subseteq x\wedge y\circ y\subseteq y\right)\to \left(x\cap y\right)\circ \left(x\cap y\right)\subseteq x\cap y$$
14	1 3 6 9 12 13	cllem0	$$⊢\forall x\in A\forall y\in Ax\cap y\in A$$