This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ∀ 𝑥 ∈ 𝐴 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 ∩ 𝑥 ∈ 𝐴 𝐵 )