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 = { z | ( z o. z ) C_ z }
Assertion	trficl	|- A. x e. A A. y e. A ( x i^i y ) e. A

Proof

Step	Hyp	Ref	Expression
1		trficl.a	|- A = { z | ( z o. z ) C_ z }
2		vex	|- x e. _V
3	2	inex1	|- ( x i^i y ) e. _V
4		id	|- ( z = ( x i^i y ) -> z = ( x i^i y ) )
5	4 4	coeq12d	|- ( z = ( x i^i y ) -> ( z o. z ) = ( ( x i^i y ) o. ( x i^i y ) ) )
6	5 4	sseq12d	|- ( z = ( x i^i y ) -> ( ( z o. z ) C_ z <-> ( ( x i^i y ) o. ( x i^i y ) ) C_ ( x i^i y ) ) )
7		id	|- ( z = x -> z = x )
8	7 7	coeq12d	|- ( z = x -> ( z o. z ) = ( x o. x ) )
9	8 7	sseq12d	|- ( z = x -> ( ( z o. z ) C_ z <-> ( x o. x ) C_ x ) )
10		id	|- ( z = y -> z = y )
11	10 10	coeq12d	|- ( z = y -> ( z o. z ) = ( y o. y ) )
12	11 10	sseq12d	|- ( z = y -> ( ( z o. z ) C_ z <-> ( y o. y ) C_ y ) )
13		trin2	|- ( ( ( x o. x ) C_ x /\ ( y o. y ) C_ y ) -> ( ( x i^i y ) o. ( x i^i y ) ) C_ ( x i^i y ) )
14	1 3 6 9 12 13	cllem0	|- A. x e. A A. y e. A ( x i^i y ) e. A