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	⊢ 𝐴 = { 𝑧 ∣ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 }
Assertion	trficl	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		trficl.a	⊢ 𝐴 = { 𝑧 ∣ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 }
2		vex	⊢ 𝑥 ∈ V
3	2	inex1	⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
4		id	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → 𝑧 = ( 𝑥 ∩ 𝑦 ) )
5	4 4	coeq12d	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∘ 𝑧 ) = ( ( 𝑥 ∩ 𝑦 ) ∘ ( 𝑥 ∩ 𝑦 ) ) )
6	5 4	sseq12d	⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( ( 𝑥 ∩ 𝑦 ) ∘ ( 𝑥 ∩ 𝑦 ) ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
8	7 7	coeq12d	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ∘ 𝑧 ) = ( 𝑥 ∘ 𝑥 ) )
9	8 7	sseq12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) )
10		id	⊢ ( 𝑧 = 𝑦 → 𝑧 = 𝑦 )
11	10 10	coeq12d	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∘ 𝑧 ) = ( 𝑦 ∘ 𝑦 ) )
12	11 10	sseq12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) )
13		trin2	⊢ ( ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ∧ ( 𝑦 ∘ 𝑦 ) ⊆ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) ∘ ( 𝑥 ∩ 𝑦 ) ) ⊆ ( 𝑥 ∩ 𝑦 ) )
14	1 3 6 9 12 13	cllem0	⊢ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 ∩ 𝑦 ) ∈ 𝐴