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 A -> Tr suc A )

Proof

Step	Hyp	Ref	Expression
1		sssucid	|- A C_ suc A
2		trel	|- ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
3	2	expd	|- ( Tr A -> ( z e. y -> ( y e. A -> z e. A ) ) )
4	3	adantrd	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> ( y e. A -> z e. A ) ) )
5		ssel	|- ( A C_ suc A -> ( z e. A -> z e. suc A ) )
6	1 4 5	ee03	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> ( y e. A -> z e. suc A ) ) )
7		simpl	|- ( ( z e. y /\ y e. suc A ) -> z e. y )
8	7	a1i	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. y ) )
9		eleq2	|- ( y = A -> ( z e. y <-> z e. A ) )
10	9	biimpcd	|- ( z e. y -> ( y = A -> z e. A ) )
11	8 10	syl6	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. A ) ) )
12	1 11 5	ee03	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) ) )
13		simpr	|- ( ( z e. y /\ y e. suc A ) -> y e. suc A )
14	13	a1i	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> y e. suc A ) )
15		elsuci	|- ( y e. suc A -> ( y e. A \/ y = A ) )
16	14 15	syl6	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) ) )
17		jao	|- ( ( y e. A -> z e. suc A ) -> ( ( y = A -> z e. suc A ) -> ( ( y e. A \/ y = A ) -> z e. suc A ) ) )
18	6 12 16 17	ee222	|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
19	18	alrimivv	|- ( Tr A -> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
20		dftr2	|- ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
21	19 20	sylibr	|- ( Tr A -> Tr suc A )