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 ∈ A Tr ⁡ B → Tr ⁡ ⋂ x ∈ A B

Proof

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