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

Proof of Theorem suctrRO
StepHypRefExpression
1   id (Tr 𝐴 → Tr 𝐴)
2   id ((𝑧𝑦𝑦 ∈ suc 𝐴) → (𝑧𝑦𝑦 ∈ suc 𝐴))
32 simpld ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧𝑦)
4   id (𝑦𝐴𝑦𝐴)
d15   trel (Tr 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
d14d15 3impib ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
d1d14 idi ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
51, 3, 4, d1 syl3an ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦𝐴) → 𝑧𝐴)
6   sssucid 𝐴 ⊆ suc 𝐴
76, 5 sseldi ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦𝐴) → 𝑧 ∈ suc 𝐴)
87 3expia ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴)) → (𝑦𝐴𝑧 ∈ suc 𝐴))
9   id (𝑦 = 𝐴𝑦 = 𝐴)
d23 adantr (((𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧𝑦)
d39 adantl (((𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴)
10d2, d3 eleqtrd (((𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧𝐴)
116, 10 sseldi (((𝑧𝑦𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)
1211 ex ((𝑧𝑦𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴𝑧 ∈ suc 𝐴))
132 simprd ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
d4   elsuci (𝑦 ∈ suc 𝐴 → (𝑦𝐴𝑦 = 𝐴))
1413, d4 syl ((𝑧𝑦𝑦 ∈ suc 𝐴) → (𝑦𝐴𝑦 = 𝐴))
d512 adantl ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴)) → (𝑦 = 𝐴𝑧 ∈ suc 𝐴))
d614 adantl ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴)) → (𝑦𝐴𝑦 = 𝐴))
158, d5, d6 mpjaod ((Tr 𝐴 ∧ (𝑧𝑦𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴)
1615 ex (Tr 𝐴 → ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
1716 alrimivv (Tr 𝐴 → ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
d16   dftr2 (Tr suc 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
d8d16 biimpri (∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
qed17, d8 syl (Tr 𝐴 → Tr suc 𝐴)
 Copyright terms: Public domain W3C validator