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

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