Theorem triin

Description: An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022)

	Ref	Expression
Assertion	triin	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
2	1	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
3		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
4		trss	⊢ ( Tr 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ⊆ 𝐵 ) )
5	4	imp	⊢ ( ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ 𝐵 )
6	5	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝐵 )
7	3 6	sylbir	⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝐵 )
8		ssiin	⊢ ( 𝑦 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝐵 )
9	7 8	sylibr	⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 )
10	2 9	sylan2b	⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ) → 𝑦 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 )
11	10	ralrimiva	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → ∀ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 𝑦 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 )
12		dftr3	⊢ ( Tr ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 𝑦 ⊆ ∩ 𝑥 ∈ 𝐴 𝐵 )
13	11 12	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∩ 𝑥 ∈ 𝐴 𝐵 )