Metamath Proof Explorer

Theorem suctrALT2VD

Description: Virtual deduction proof of suctrALT2 . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion suctrALT2VD 
|- ( Tr A -> Tr suc A )

Proof

Step Hyp Ref Expression
1 dftr2 
 |-  ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) )
2 sssucid 
 |-  A C_ suc A
3 idn1 
 |-  (. Tr A ->. Tr A ).
4 idn2 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. ( z e. y /\ y e. suc A ) ).
5 simpl 
 |-  ( ( z e. y /\ y e. suc A ) -> z e. y )
6 4 5 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. z e. y ).
7 idn3 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y e. A ->. y e. A ).
8 trel 
 |-  ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) )
9 8 expd 
 |-  ( Tr A -> ( z e. y -> ( y e. A -> z e. A ) ) )
10 3 6 7 9 e123 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y e. A ->. z e. A ).
11 ssel 
 |-  ( A C_ suc A -> ( z e. A -> z e. suc A ) )
12 2 10 11 e03 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y e. A ->. z e. suc A ).
13 12 in3 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. ( y e. A -> z e. suc A ) ).
14 idn3 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y = A ->. y = A ).
15 eleq2 
 |-  ( y = A -> ( z e. y <-> z e. A ) )
16 15 biimpcd 
 |-  ( z e. y -> ( y = A -> z e. A ) )
17 6 14 16 e23 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y = A ->. z e. A ).
18 2 17 11 e03 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ,. y = A ->. z e. suc A ).
19 18 in3 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
20 simpr 
 |-  ( ( z e. y /\ y e. suc A ) -> y e. suc A )
21 4 20 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. y e. suc A ).
22 elsuci 
 |-  ( y e. suc A -> ( y e. A \/ y = A ) )
23 21 22 e2 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
24 jao 
 |-  ( ( y e. A -> z e. suc A ) -> ( ( y = A -> z e. suc A ) -> ( ( y e. A \/ y = A ) -> z e. suc A ) ) )
25 13 19 23 24 e222 
 |-  (. Tr A ,. ( z e. y /\ y e. suc A ) ->. z e. suc A ).
26 25 in2 
 |-  (. Tr A ->. ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
27 26 gen12 
 |-  (. Tr A ->. A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
28 biimpr 
 |-  ( ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ) -> ( A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) -> Tr suc A ) )
29 1 27 28 e01 
 |-  (. Tr A ->. Tr suc A ).
30 29 in1 
 |-  ( Tr A -> Tr suc A )