Theorem suctrALT 39880

Description: The successor of a transitive class is transitive. The proof of http://us.metamath.org/other/completeusersproof/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctrALT 39880 using completeusersproof, which is verified by the Metamath program. The proof of http://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 6046 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.)

Assertion

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

Proof of Theorem suctrALT

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sssucid 6040	. . . . . . 7 ⊢ 𝐴 ⊆ suc 𝐴
2		id 22	. . . . . . . 8 ⊢ (Tr 𝐴 → Tr 𝐴)
3		id 22	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴))
4	3	simpld 490	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦)
5		id 22	. . . . . . . 8 ⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴)
6		trel 4982	. . . . . . . . . 10 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
7	6	3impib 1150	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
8	7	idiALT 39521	. . . . . . . 8 ⊢ ((Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
9	2, 4, 5, 8	syl3an 1205	. . . . . . 7 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
10	1, 9	sseldi 3825	. . . . . 6 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ suc 𝐴)
11	10	3expia 1156	. . . . 5 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴))
12	4	adantr 474	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝑦)
13		id 22	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → 𝑦 = 𝐴)
14	13	adantl 475	. . . . . . . . 9 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑦 = 𝐴)
15	12, 14	eleqtrd 2908	. . . . . . . 8 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴)
16	1, 15	sseldi 3825	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) ∧ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)
17	16	ex 403	. . . . . 6 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴))
18	17	adantl 475	. . . . 5 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴))
19	3	simprd 491	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
20		elsuci 6029	. . . . . . 7 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
21	19, 20	syl 17	. . . . . 6 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
22	21	adantl 475	. . . . 5 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
23	11, 18, 22	mpjaod 893	. . . 4 ⊢ ((Tr 𝐴 ∧ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)) → 𝑧 ∈ suc 𝐴)
24	23	ex 403	. . 3 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
25	24	alrimivv 2029	. 2 ⊢ (Tr 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
26		dftr2 4977	. . 3 ⊢ (Tr suc 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
27	26	biimpri 220	. 2 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
28	25, 27	syl 17	1 ⊢ (Tr 𝐴 → Tr suc 𝐴)

Syntax hints:   → wi 4   ∧ wa 386   ∨ wo 880   ∧ w3a 1113  ∀wal 1656   = wceq 1658   ∈ wcel 2166  Tr wtr 4975  suc csuc 5965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-in 3805  df-ss 3812  df-sn 4398  df-uni 4659  df-tr 4976  df-suc 5969

This theorem is referenced by: (None)