Metamath Proof Explorer

Theorem suctrALT

Description: The successor of a transitive class is transitive. The proof of https://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. See suctr for the original proof. (Contributed by Alan Sare, 11-Apr-2009) (Revised by Alan Sare, 12-Jun-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT ( Tr 𝐴 → Tr suc 𝐴 )

Proof

Step Hyp Ref Expression
1 sssucid ⊢ 𝐴 ⊆ suc 𝐴
2 id ⊢ ( Tr 𝐴 → Tr 𝐴 )
3 id ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) )
4 3 simpld ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
5 id ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 )
6 trel ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
7 6 3impib ⊢ ( ( Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
8 7 idiALT ⊢ ( ( Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
9 2 4 5 8 syl3an ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
10 1 9 sselid ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ suc 𝐴 )
11 10 3expia ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) )
12 4 adantr ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝑦 )
13 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
14 13 adantl ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
15 12 14 eleqtrd ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
16 1 15 sselid ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 )
17 16 ex ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) )
18 17 adantl ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) )
19 3 simprd ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
20 elsuci ⊢ ( 𝑦 ∈ suc 𝐴 → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
21 19 20 syl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
22 21 adantl ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
23 11 18 22 mpjaod ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
24 23 ex ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
25 24 alrimivv ⊢ ( Tr 𝐴 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
26 dftr2 ⊢ ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
27 26 biimpri ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) → Tr suc 𝐴 )
28 25 27 syl ⊢ ( Tr 𝐴 → Tr suc 𝐴 )