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	|- ( ph -> R We A )
	wsuclb.2	|- ( ph -> R Se A )
	wsuclb.3	|- ( ph -> X e. V )
	wsuclb.4	|- ( ph -> Y e. A )
	wsuclb.5	|- ( ph -> X R Y )
Assertion	wsuclb	|- ( ph -> -. Y R wsuc ( R , A , X ) )

Proof

Step	Hyp	Ref	Expression
1		wsuclb.1	|- ( ph -> R We A )
2		wsuclb.2	|- ( ph -> R Se A )
3		wsuclb.3	|- ( ph -> X e. V )
4		wsuclb.4	|- ( ph -> Y e. A )
5		wsuclb.5	|- ( ph -> X R Y )
6		brcnvg	|- ( ( Y e. A /\ X e. V ) -> ( Y `' R X <-> X R Y ) )
7	4 3 6	syl2anc	|- ( ph -> ( Y `' R X <-> X R Y ) )
8	5 7	mpbird	|- ( ph -> Y `' R X )
9		elpredg	|- ( ( X e. V /\ Y e. A ) -> ( Y e. Pred ( `' R , A , X ) <-> Y `' R X ) )
10	3 4 9	syl2anc	|- ( ph -> ( Y e. Pred ( `' R , A , X ) <-> Y `' R X ) )
11	8 10	mpbird	|- ( ph -> Y e. Pred ( `' R , A , X ) )
12		weso	|- ( R We A -> R Or A )
13	1 12	syl	|- ( ph -> R Or A )
14		breq2	|- ( y = Y -> ( X R y <-> X R Y ) )
15	14	rspcev	|- ( ( Y e. A /\ X R Y ) -> E. y e. A X R y )
16	4 5 15	syl2anc	|- ( ph -> E. y e. A X R y )
17	1 2 3 16	wsuclem	|- ( ph -> E. a e. A ( A. b e. Pred ( `' R , A , X ) -. b R a /\ A. b e. A ( a R b -> E. c e. Pred ( `' R , A , X ) c R b ) ) )
18	13 17	inflb	|- ( ph -> ( Y e. Pred ( `' R , A , X ) -> -. Y R inf ( Pred ( `' R , A , X ) , A , R ) ) )
19	11 18	mpd	|- ( ph -> -. Y R inf ( Pred ( `' R , A , X ) , A , R ) )
20		df-wsuc	|- wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
21	20	breq2i	|- ( Y R wsuc ( R , A , X ) <-> Y R inf ( Pred ( `' R , A , X ) , A , R ) )
22	19 21	sylnibr	|- ( ph -> -. Y R wsuc ( R , A , X ) )