Metamath Proof Explorer

Theorem suctr

Description: The successor of a transitive class is transitive. (Contributed by Alan Sare, 11-Apr-2009) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion suctr ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 elsuci ⊢ y ∈ suc ⁡ A → y ∈ A ∨ y = A
2 trel ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ A → z ∈ A
3 2 expdimp ⊢ Tr ⁡ A ∧ z ∈ y → y ∈ A → z ∈ A
4 eleq2 ⊢ y = A → z ∈ y ↔ z ∈ A
5 4 biimpcd ⊢ z ∈ y → y = A → z ∈ A
6 5 adantl ⊢ Tr ⁡ A ∧ z ∈ y → y = A → z ∈ A
7 3 6 jaod ⊢ Tr ⁡ A ∧ z ∈ y → y ∈ A ∨ y = A → z ∈ A
8 1 7 syl5 ⊢ Tr ⁡ A ∧ z ∈ y → y ∈ suc ⁡ A → z ∈ A
9 8 expimpd ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ A
10 elelsuc ⊢ z ∈ A → z ∈ suc ⁡ A
11 9 10 syl6 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
12 11 alrimivv ⊢ Tr ⁡ A → ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
13 dftr2 ⊢ Tr ⁡ suc ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
14 12 13 sylibr ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A