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
| 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 𝐴) )
| | qed | 17 | ⊢ ( Tr 𝐴 ▶ Tr suc 𝐴 )
|
|