Metamath Proof Explorer

Theorem suctrALT3

Description: The successor of a transitive class is transitive. suctrALT3 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html . It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded ). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 ) . (Contributed by Alan Sare, 3-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT3 ( Tr 𝐴 → Tr suc 𝐴 )

Proof

Step Hyp Ref Expression
1 sssucid ⊢ 𝐴 ⊆ suc 𝐴
2 id ⊢ ( Tr 𝐴 → Tr 𝐴 )
3 id ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) )
4 3 simpld ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
5 id ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 )
6 2 4 5 trelded ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
7 1 6 sselid ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ suc 𝐴 )
8 7 3expia ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) )
9 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
10 eleq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴 ) )
11 10 biimpac ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
12 4 9 11 syl2an ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
13 1 12 sselid ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 )
14 13 ex ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) )
15 3 simprd ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
16 elsuci ⊢ ( 𝑦 ∈ suc 𝐴 → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
17 15 16 syl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
18 8 14 17 jaoded ⊢ ( ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
19 18 un2122 ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
20 19 ex ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
21 20 alrimivv ⊢ ( Tr 𝐴 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
22 dftr2 ⊢ ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
23 22 biimpri ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) → Tr suc 𝐴 )
24 21 23 syl ⊢ ( Tr 𝐴 → Tr suc 𝐴 )
25 24 idiALT ⊢ ( Tr 𝐴 → Tr suc 𝐴 )