Theorem suctrALT4VD
Description: The sucessor of a transitive class is transitive. The proof of suctralt3VD is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT4 using completeusersproof, which is verified by the Metamath program. The proof of suctrALT4RO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 3-Apr-2016.) (Formatting changes made by Alan Sare on 10-Jun-2018.)
Assertion
Ref Expression
suctrALT4VD (Tr 𝐴 → Tr suc 𝐴)

Proof of Theorem suctrALT4VD
StepHypExpression
1  (   Tr 𝐴   ▶   Tr 𝐴   )
2  (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
32 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑧𝑦   )
4  (   𝑦𝐴   ▶   𝑦𝐴   )
51, 3, 4 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧𝐴   )
6  𝐴 ⊆ suc 𝐴
75, 6 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
87 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
9  (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
103, 9 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧𝐴   )
1110, 6 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1211 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
132 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
1413 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
158, 12, 14 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
1615 (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
1716 (   Tr 𝐴   ▶   𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
1817 (   Tr 𝐴   ▶   Tr suc 𝐴   )
qed18 (Tr 𝐴 → Tr suc 𝐴)
 Copyright terms: Public domain W3C validator