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 𝐴 → Tr suc 𝐴 )

Proof

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