Step |
Hyp |
Ref |
Expression |
1 |
|
sssucid |
|- A C_ suc A |
2 |
|
id |
|- ( Tr A -> Tr A ) |
3 |
|
id |
|- ( ( z e. y /\ y e. suc A ) -> ( z e. y /\ y e. suc A ) ) |
4 |
3
|
simpld |
|- ( ( z e. y /\ y e. suc A ) -> z e. y ) |
5 |
|
id |
|- ( y e. A -> y e. A ) |
6 |
|
trel |
|- ( Tr A -> ( ( z e. y /\ y e. A ) -> z e. A ) ) |
7 |
6
|
3impib |
|- ( ( Tr A /\ z e. y /\ y e. A ) -> z e. A ) |
8 |
7
|
idiALT |
|- ( ( Tr A /\ z e. y /\ y e. A ) -> z e. A ) |
9 |
2 4 5 8
|
syl3an |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. A ) |
10 |
1 9
|
sseldi |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) /\ y e. A ) -> z e. suc A ) |
11 |
10
|
3expia |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A -> z e. suc A ) ) |
12 |
4
|
adantr |
|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. y ) |
13 |
|
id |
|- ( y = A -> y = A ) |
14 |
13
|
adantl |
|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> y = A ) |
15 |
12 14
|
eleqtrd |
|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. A ) |
16 |
1 15
|
sseldi |
|- ( ( ( z e. y /\ y e. suc A ) /\ y = A ) -> z e. suc A ) |
17 |
16
|
ex |
|- ( ( z e. y /\ y e. suc A ) -> ( y = A -> z e. suc A ) ) |
18 |
17
|
adantl |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y = A -> z e. suc A ) ) |
19 |
3
|
simprd |
|- ( ( z e. y /\ y e. suc A ) -> y e. suc A ) |
20 |
|
elsuci |
|- ( y e. suc A -> ( y e. A \/ y = A ) ) |
21 |
19 20
|
syl |
|- ( ( z e. y /\ y e. suc A ) -> ( y e. A \/ y = A ) ) |
22 |
21
|
adantl |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> ( y e. A \/ y = A ) ) |
23 |
11 18 22
|
mpjaod |
|- ( ( Tr A /\ ( z e. y /\ y e. suc A ) ) -> z e. suc A ) |
24 |
23
|
ex |
|- ( Tr A -> ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ) |
25 |
24
|
alrimivv |
|- ( Tr A -> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ) |
26 |
|
dftr2 |
|- ( Tr suc A <-> A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ) |
27 |
26
|
biimpri |
|- ( A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) -> Tr suc A ) |
28 |
25 27
|
syl |
|- ( Tr A -> Tr suc A ) |