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⁡A→Tr⁡suc⁡A

Proof

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