Metamath Proof Explorer

Theorem triin

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

Ref Expression
Assertion triin ⊢∀x∈ATr⁡B→Tr⁡⋂x∈AB

Proof

Step Hyp Ref Expression
1 eliin ⊢y∈V→y∈⋂x∈AB↔∀x∈Ay∈B
2 1 elv ⊢y∈⋂x∈AB↔∀x∈Ay∈B
3 r19.26 ⊢∀x∈ATr⁡B∧y∈B↔∀x∈ATr⁡B∧∀x∈Ay∈B
4 trss ⊢Tr⁡B→y∈B→y⊆B
5 4 imp ⊢Tr⁡B∧y∈B→y⊆B
6 5 ralimi ⊢∀x∈ATr⁡B∧y∈B→∀x∈Ay⊆B
7 3 6 sylbir ⊢∀x∈ATr⁡B∧∀x∈Ay∈B→∀x∈Ay⊆B
8 ssiin ⊢y⊆⋂x∈AB↔∀x∈Ay⊆B
9 7 8 sylibr ⊢∀x∈ATr⁡B∧∀x∈Ay∈B→y⊆⋂x∈AB
10 2 9 sylan2b ⊢∀x∈ATr⁡B∧y∈⋂x∈AB→y⊆⋂x∈AB
11 10 ralrimiva ⊢∀x∈ATr⁡B→∀y∈⋂x∈ABy⊆⋂x∈AB
12 dftr3 ⊢Tr⁡⋂x∈AB↔∀y∈⋂x∈ABy⊆⋂x∈AB
13 11 12 sylibr ⊢∀x∈ATr⁡B→Tr⁡⋂x∈AB