Metamath Proof Explorer

Theorem suctrALTcf

Description: The sucessor of a transitive class is transitive. suctrALTcf , using conventional notation, was translated from virtual deduction form, suctrALTcfVD , using a translation program. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALTcf ⊢ 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 simpl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
5 3 4 syl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
6 id ⊢ y ∈ A → y ∈ A
7 trel ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ A → z ∈ A
8 7 3impib ⊢ Tr ⁡ A ∧ z ∈ y ∧ y ∈ A → z ∈ A
9 2 5 6 8 syl3an ⊢ Tr ⁡ A ∧ z ∈ y ∧ y ∈ suc ⁡ A ∧ y ∈ A → z ∈ A
10 ssel2 ⊢ A ⊆ suc ⁡ A ∧ z ∈ A → z ∈ suc ⁡ A
11 1 9 10 eel0321old ⊢ Tr ⁡ A ∧ z ∈ y ∧ y ∈ suc ⁡ A ∧ y ∈ A → z ∈ suc ⁡ A
12 11 3expia ⊢ Tr ⁡ A ∧ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A → z ∈ suc ⁡ A
13 id ⊢ y = A → y = A
14 eleq2 ⊢ y = A → z ∈ y ↔ z ∈ A
15 14 biimpac ⊢ z ∈ y ∧ y = A → z ∈ A
16 5 13 15 syl2an ⊢ z ∈ y ∧ y ∈ suc ⁡ A ∧ y = A → z ∈ A
17 1 16 10 eel021old ⊢ z ∈ y ∧ y ∈ suc ⁡ A ∧ y = A → z ∈ suc ⁡ A
18 17 ex ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A
19 simpr ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
20 3 19 syl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
21 elsuci ⊢ y ∈ suc ⁡ A → y ∈ A ∨ y = A
22 20 21 syl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A ∨ y = A
23 jao ⊢ y ∈ A → z ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A → y ∈ A ∨ y = A → z ∈ suc ⁡ A
24 23 3imp ⊢ y ∈ A → z ∈ suc ⁡ A ∧ y = A → z ∈ suc ⁡ A ∧ y ∈ A ∨ y = A → z ∈ suc ⁡ A
25 12 18 22 24 eel2122old ⊢ Tr ⁡ A ∧ z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
26 25 ex ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
27 26 alrimivv ⊢ Tr ⁡ A → ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
28 dftr2 ⊢ Tr ⁡ suc ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
29 28 biimpri ⊢ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A → Tr ⁡ suc ⁡ A
30 27 29 syl ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A
31 30 iin1 ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A