Description: A well-founded successor is a lower bound on points after X . (Contributed by Scott Fenton, 16-Jun-2018) (Proof shortened by AV, 10-Oct-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | wsuclb.1 | |
|
wsuclb.2 | |
||
wsuclb.3 | |
||
wsuclb.4 | |
||
wsuclb.5 | |
||
Assertion | wsuclb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wsuclb.1 | |
|
2 | wsuclb.2 | |
|
3 | wsuclb.3 | |
|
4 | wsuclb.4 | |
|
5 | wsuclb.5 | |
|
6 | brcnvg | |
|
7 | 4 3 6 | syl2anc | |
8 | 5 7 | mpbird | |
9 | elpredg | |
|
10 | 3 4 9 | syl2anc | |
11 | 8 10 | mpbird | |
12 | weso | |
|
13 | 1 12 | syl | |
14 | breq2 | |
|
15 | 14 | rspcev | |
16 | 4 5 15 | syl2anc | |
17 | 1 2 3 16 | wsuclem | |
18 | 13 17 | inflb | |
19 | 11 18 | mpd | |
20 | df-wsuc | |
|
21 | 20 | breq2i | |
22 | 19 21 | sylnibr | |