Theorem suctrVD
Description: The sucessor of a transitive class is transitive. The proof of suctrVD is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctr using completeusersproof, which is verified by the Metamath program. The proof of suctrRO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare on 13-Jun-2018.)
Assertion
Ref Expression
suctrVD (   Tr 𝐴   ▶   Tr suc 𝐴   )

Proof of Theorem suctrVD
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 𝐴)   )
qed17 (   Tr 𝐴   ▶   Tr suc 𝐴   )
 Copyright terms: Public domain W3C validator