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

Metamath Proof Explorer

Theorem trsuc

Description: A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion trsuc ⊢ Tr ⁡ A ∧ suc ⁡ B ∈ A → B ∈ A

Proof

Step Hyp Ref Expression
1 trel ⊢ Tr ⁡ A → B ∈ suc ⁡ B ∧ suc ⁡ B ∈ A → B ∈ A
2 sssucid ⊢ B ⊆ suc ⁡ B
3 ssexg ⊢ B ⊆ suc ⁡ B ∧ suc ⁡ B ∈ A → B ∈ V
4 2 3 mpan ⊢ suc ⁡ B ∈ A → B ∈ V
5 sucidg ⊢ B ∈ V → B ∈ suc ⁡ B
6 4 5 syl ⊢ suc ⁡ B ∈ A → B ∈ suc ⁡ B
7 6 ancri ⊢ suc ⁡ B ∈ A → B ∈ suc ⁡ B ∧ suc ⁡ B ∈ A
8 1 7 impel ⊢ Tr ⁡ A ∧ suc ⁡ B ∈ A → B ∈ A