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	$⊢ φ \to R We A$
	wsuclb.2	$⊢ φ \to R Se A$
	wsuclb.3	$⊢ φ \to X \in V$
	wsuclb.4	$⊢ φ \to Y \in A$
	wsuclb.5	$⊢ φ \to X R Y$
Assertion	wsuclb	$⊢ φ \to \neg Y R wsuc (R, A, X)$

Proof

Step	Hyp	Ref	Expression
1		wsuclb.1	$⊢ φ \to R We A$
2		wsuclb.2	$⊢ φ \to R Se A$
3		wsuclb.3	$⊢ φ \to X \in V$
4		wsuclb.4	$⊢ φ \to Y \in A$
5		wsuclb.5	$⊢ φ \to X R Y$
6		brcnvg	$⊢ (Y \in A \land X \in V) \to (Y R^{-1} X \leftrightarrow X R Y)$
7	4 3 6	syl2anc	$⊢ φ \to (Y R^{-1} X \leftrightarrow X R Y)$
8	5 7	mpbird	$⊢ φ \to Y R^{-1} X$
9		elpredg	$⊢ (X \in V \land Y \in A) \to (Y \in Pred (R^{-1}, A, X) \leftrightarrow Y R^{-1} X)$
10	3 4 9	syl2anc	$⊢ φ \to (Y \in Pred (R^{-1}, A, X) \leftrightarrow Y R^{-1} X)$
11	8 10	mpbird	$⊢ φ \to Y \in Pred (R^{-1}, A, X)$
12		weso	$⊢ R We A \to R Or A$
13	1 12	syl	$⊢ φ \to R Or A$
14		breq2	$⊢ y = Y \to (X R y \leftrightarrow X R Y)$
15	14	rspcev	$⊢ (Y \in A \land X R Y) \to \exists y \in A X R y$
16	4 5 15	syl2anc	$⊢ φ \to \exists y \in A X R y$
17	1 2 3 16	wsuclem	$⊢ φ \to \exists a \in A (\forall b \in Pred (R^{-1}, A, X) \neg b R a \land \forall b \in A (a R b \to \exists c \in Pred (R^{-1}, A, X) c R b))$
18	13 17	inflb	$⊢ φ \to (Y \in Pred (R^{-1}, A, X) \to \neg Y R inf (Pred (R^{-1}, A, X), A, R))$
19	11 18	mpd	$⊢ φ \to \neg Y R inf (Pred (R^{-1}, A, X), A, R)$
20		df-wsuc	$⊢ wsuc (R, A, X) = inf (Pred (R^{-1}, A, X), A, R)$
21	20	breq2i	$⊢ Y R wsuc (R, A, X) \leftrightarrow Y R inf (Pred (R^{-1}, A, X), A, R)$
22	19 21	sylnibr	$⊢ φ \to \neg Y R wsuc (R, A, X)$

Metamath Proof Explorer

Theorem wsuclb

Proof