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

Proof

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