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
| Step | Hyp | Expression |
|---|
| 1 | | ⊢ ( Tr 𝐴 ▶ Tr 𝐴 )
| | 2 | | ⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) )
| | 3 | 2 | ⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑧 ∈ 𝑦 )
| | 4 | | ⊢ ( 𝑦 ∈ 𝐴 ▶ 𝑦 ∈ 𝐴 )
| | 5 | 1, 3, 4 | ⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
| | 6 | | ⊢ 𝐴 ⊆ suc 𝐴
| | 7 | 5, 6 | ⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
| | 8 | 7 | ⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) )
| | 9 | | ⊢ ( 𝑦 = 𝐴 ▶ 𝑦 = 𝐴 )
| | 10 | 3, 9 | ⊢ ( ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
| | 11 | 10, 6 | ⊢ ( ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
| | 12 | 11 | ⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) )
| | 13 | 2 | ⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ 𝑦 ∈ suc 𝐴 )
| | 14 | 13 | ⊢ ( (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ▶ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) )
| | 15 | 8, 12, 14 | ⊢ ( ( Tr 𝐴 , (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ) ▶ 𝑧 ∈ suc 𝐴 )
| | 16 | 15 | ⊢ ( Tr 𝐴 ▶ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) )
| | 17 | 16 | ⊢ ( Tr 𝐴 ▶ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) )
| | 18 | 17 | ⊢ ( Tr 𝐴 ▶ Tr suc 𝐴 )
| | qed | 18 | ⊢ (Tr 𝐴 → Tr suc 𝐴)
|
|