Metamath Proof Explorer

Theorem suctrALT2VD

Description: Virtual deduction proof of suctrALT2 . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 dftr2 ⊢ Tr ⁡ suc ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
2 sssucid ⊢ A ⊆ suc ⁡ A
3 idn1 ⊢ Tr ⁡ A → Tr ⁡ A
4 idn2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A
5 simpl ⊢ z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
6 4 5 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → z ∈ y
7 idn3 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y ∈ A → y ∈ A
8 trel ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ A → z ∈ A
9 8 expd ⊢ Tr ⁡ A → z ∈ y → y ∈ A → z ∈ A
10 3 6 7 9 e123 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y ∈ A → z ∈ A
11 ssel ⊢ A ⊆ suc ⁡ A → z ∈ A → z ∈ suc ⁡ A
12 2 10 11 e03 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y ∈ A → z ∈ suc ⁡ A
13 12 in3 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A → z ∈ suc ⁡ A
14 idn3 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y = A → y = A
15 eleq2 ⊢ y = A → z ∈ y ↔ z ∈ A
16 15 biimpcd ⊢ z ∈ y → y = A → z ∈ A
17 6 14 16 e23 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y = A → z ∈ A
18 2 17 11 e03 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A , y = A → z ∈ suc ⁡ A
19 18 in3 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A
20 simpr ⊢ z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
21 4 20 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → y ∈ suc ⁡ A
22 elsuci ⊢ y ∈ suc ⁡ A → y ∈ A ∨ y = A
23 21 22 e2 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → y ∈ A ∨ y = A
24 jao ⊢ y ∈ A → z ∈ suc ⁡ A → y = A → z ∈ suc ⁡ A → y ∈ A ∨ y = A → z ∈ suc ⁡ A
25 13 19 23 24 e222 ⊢ Tr ⁡ A , z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
26 25 in2 ⊢ Tr ⁡ A → z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
27 26 gen12 ⊢ Tr ⁡ A → ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A
28 biimpr ⊢ Tr ⁡ suc ⁡ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A → ∀ z ∀ y z ∈ y ∧ y ∈ suc ⁡ A → z ∈ suc ⁡ A → Tr ⁡ suc ⁡ A
29 1 27 28 e01 ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A
30 29 in1 ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A