Metamath Proof Explorer

Theorem suctrALT2

Description: Virtual deduction proof of suctr . The sucessor of a transitive class is transitive. This proof was generated automatically from the virtual deduction proof suctrALT2VD using the tools command file translate__without__overwriting__minimize__excluding__duplicates.cmd . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT2 ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A

Proof

Step Hyp Ref Expression
1 sssucid ⊢ A ⊆ suc ⁡ A
2 trel ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ A → z ∈ A
3 2 expd ⊢ Tr ⁡ A → z ∈ y → y ∈ A → z ∈ A
4 3 adantrd ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A → z ∈ A
5 ssel ⊢ A ⊆ suc ⁡ A → z ∈ A → z ∈ suc ⁡ A
6 1 4 5 ee03 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A → z ∈ suc ⁡ A
7 simpl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
8 7 a1i ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
9 eleq2 ⊢ y = A → z ∈ y ↔ z ∈ A
10 9 biimpcd ⊢ z ∈ y → y = A → z ∈ A
11 8 10 syl6 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y = A → z ∈ A
12 1 11 5 ee03 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A
13 simpr ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
14 13 a1i ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
15 elsuci ⊢ y ∈ suc ⁡ A → y ∈ A ∨ y = A
16 14 15 syl6 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A ∨ y = A
17 jao ⊢ y ∈ A → z ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A → y ∈ A ∨ y = A → z ∈ suc ⁡ A
18 6 12 16 17 ee222 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
19 18 alrimivv ⊢ Tr ⁡ A → ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
20 dftr2 ⊢ Tr ⁡ suc ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
21 19 20 sylibr ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A