Metamath Proof Explorer


Theorem wsuclb

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 φRWeA
wsuclb.2 φRSeA
wsuclb.3 φXV
wsuclb.4 φYA
wsuclb.5 φXRY
Assertion wsuclb φ¬YRwsucRAX

Proof

Step Hyp Ref Expression
1 wsuclb.1 φRWeA
2 wsuclb.2 φRSeA
3 wsuclb.3 φXV
4 wsuclb.4 φYA
5 wsuclb.5 φXRY
6 brcnvg YAXVYR-1XXRY
7 4 3 6 syl2anc φYR-1XXRY
8 5 7 mpbird φYR-1X
9 elpredg XVYAYPredR-1AXYR-1X
10 3 4 9 syl2anc φYPredR-1AXYR-1X
11 8 10 mpbird φYPredR-1AX
12 weso RWeAROrA
13 1 12 syl φROrA
14 breq2 y=YXRyXRY
15 14 rspcev YAXRYyAXRy
16 4 5 15 syl2anc φyAXRy
17 1 2 3 16 wsuclem φaAbPredR-1AX¬bRabAaRbcPredR-1AXcRb
18 13 17 inflb φYPredR-1AX¬YRsupPredR-1AXAR
19 11 18 mpd φ¬YRsupPredR-1AXAR
20 df-wsuc wsucRAX=supPredR-1AXAR
21 20 breq2i YRwsucRAXYRsupPredR-1AXAR
22 19 21 sylnibr φ¬YRwsucRAX