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 𝐴 → Tr suc 𝐴 )

Proof

Step Hyp Ref Expression
1 sssucid ⊢ 𝐴 ⊆ suc 𝐴
2 id ⊢ ( Tr 𝐴 → Tr 𝐴 )
3 id ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) )
4 simpl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
5 3 4 syl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
6 id ⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐴 )
7 trel ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
8 7 3impib ⊢ ( ( Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
9 2 5 6 8 syl3an ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
10 ssel2 ⊢ ( ( 𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ suc 𝐴 )
11 1 9 10 eel0321old ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ suc 𝐴 )
12 11 3expia ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) )
13 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
14 eleq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴 ) )
15 14 biimpac ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
16 5 13 15 syl2an ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
17 1 16 10 eel021old ⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 )
18 17 ex ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) )
19 simpr ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
20 3 19 syl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
21 elsuci ⊢ ( 𝑦 ∈ suc 𝐴 → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
22 20 21 syl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
23 jao ⊢ ( ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 ) ) )
24 23 3imp ⊢ ( ( ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) ∧ ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
25 12 18 22 24 eel2122old ⊢ ( ( Tr 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
26 25 ex ⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
27 26 alrimivv ⊢ ( Tr 𝐴 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
28 dftr2 ⊢ ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
29 28 biimpri ⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) → Tr suc 𝐴 )
30 27 29 syl ⊢ ( Tr 𝐴 → Tr suc 𝐴 )
31 30 iin1 ⊢ ( Tr 𝐴 → Tr suc 𝐴 )