wsuclem

Description: Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Hypotheses	wsuclem.1	$⊢ φ \to R We A$
	wsuclem.2	$⊢ φ \to R Se A$
	wsuclem.3	$⊢ φ \to X \in V$
	wsuclem.4	$⊢ φ \to \exists w \in A X R w$
Assertion	wsuclem	$⊢ φ \to \exists x \in A (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y))$

Proof

Step	Hyp	Ref	Expression
1		wsuclem.1	$⊢ φ \to R We A$
2		wsuclem.2	$⊢ φ \to R Se A$
3		wsuclem.3	$⊢ φ \to X \in V$
4		wsuclem.4	$⊢ φ \to \exists w \in A X R w$
5		predss	$⊢ Pred (R^{-1}, A, X) \subseteq A$
6	5	a1i	$⊢ φ \to Pred (R^{-1}, A, X) \subseteq A$
7		dfpred3g	$⊢ X \in V \to Pred (R^{-1}, A, X) = \{w \in A \| w R^{-1} X\}$
8	3 7	syl	$⊢ φ \to Pred (R^{-1}, A, X) = \{w \in A \| w R^{-1} X\}$
9	3	elexd	$⊢ φ \to X \in V$
10		rabn0	$⊢ \{w \in A \| w R^{-1} X\} \neq \emptyset \leftrightarrow \exists w \in A w R^{-1} X$
11		brcnvg	$⊢ (w \in A \land X \in V) \to (w R^{-1} X \leftrightarrow X R w)$
12	11	ancoms	$⊢ (X \in V \land w \in A) \to (w R^{-1} X \leftrightarrow X R w)$
13	12	rexbidva	$⊢ X \in V \to (\exists w \in A w R^{-1} X \leftrightarrow \exists w \in A X R w)$
14	10 13	bitrid	$⊢ X \in V \to (\{w \in A \| w R^{-1} X\} \neq \emptyset \leftrightarrow \exists w \in A X R w)$
15	14	biimpar	$⊢ (X \in V \land \exists w \in A X R w) \to \{w \in A \| w R^{-1} X\} \neq \emptyset$
16	9 4 15	syl2anc	$⊢ φ \to \{w \in A \| w R^{-1} X\} \neq \emptyset$
17	8 16	eqnetrd	$⊢ φ \to Pred (R^{-1}, A, X) \neq \emptyset$
18		tz6.26	$⊢ ((R We A \land R Se A) \land (Pred (R^{-1}, A, X) \subseteq A \land Pred (R^{-1}, A, X) \neq \emptyset)) \to \exists x \in Pred (R^{-1}, A, X) Pred (R, Pred (R^{-1}, A, X), x) = \emptyset$
19	1 2 6 17 18	syl22anc	$⊢ φ \to \exists x \in Pred (R^{-1}, A, X) Pred (R, Pred (R^{-1}, A, X), x) = \emptyset$
20		dfpred3g	$⊢ X \in V \to Pred (R^{-1}, A, X) = \{y \in A \| y R^{-1} X\}$
21	3 20	syl	$⊢ φ \to Pred (R^{-1}, A, X) = \{y \in A \| y R^{-1} X\}$
22	21	rexeqdv	$⊢ φ \to (\exists x \in Pred (R^{-1}, A, X) Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \leftrightarrow \exists x \in \{y \in A \| y R^{-1} X\} Pred (R, Pred (R^{-1}, A, X), x) = \emptyset)$
23		breq1	$⊢ y = x \to (y R^{-1} X \leftrightarrow x R^{-1} X)$
24	23	rexrab	$⊢ \exists x \in \{y \in A \| y R^{-1} X\} Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \leftrightarrow \exists x \in A (x R^{-1} X \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset)$
25		noel	$⊢ \neg y \in \emptyset$
26		simp2r	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to Pred (R, Pred (R^{-1}, A, X), x) = \emptyset$
27	26	eleq2d	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to (y \in Pred (R, Pred (R^{-1}, A, X), x) \leftrightarrow y \in \emptyset)$
28	25 27	mtbiri	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to \neg y \in Pred (R, Pred (R^{-1}, A, X), x)$
29		vex	$⊢ x \in V$
30	29	a1i	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to x \in V$
31		simp3	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to y \in Pred (R^{-1}, A, X)$
32		elpredg	$⊢ (x \in V \land y \in Pred (R^{-1}, A, X)) \to (y \in Pred (R, Pred (R^{-1}, A, X), x) \leftrightarrow y R x)$
33	30 31 32	syl2anc	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to (y \in Pred (R, Pred (R^{-1}, A, X), x) \leftrightarrow y R x)$
34	28 33	mtbid	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \land y \in Pred (R^{-1}, A, X)) \to \neg y R x$
35	34	3expa	$⊢ ((φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset)) \land y \in Pred (R^{-1}, A, X)) \to \neg y R x$
36	35	ralrimiva	$⊢ (φ \land (x \in A \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset)) \to \forall y \in Pred (R^{-1}, A, X) \neg y R x$
37	36	expr	$⊢ (φ \land x \in A) \to (Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \to \forall y \in Pred (R^{-1}, A, X) \neg y R x)$
38		simp1rl	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to x \in A$
39		simp1rr	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to x R^{-1} X$
40	3	adantr	$⊢ (φ \land (x \in A \land x R^{-1} X)) \to X \in V$
41	40	3ad2ant1	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to X \in V$
42	29	elpred	$⊢ X \in V \to (x \in Pred (R^{-1}, A, X) \leftrightarrow (x \in A \land x R^{-1} X))$
43	41 42	syl	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to (x \in Pred (R^{-1}, A, X) \leftrightarrow (x \in A \land x R^{-1} X))$
44	38 39 43	mpbir2and	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to x \in Pred (R^{-1}, A, X)$
45		simp3	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to x R y$
46		breq1	$⊢ z = x \to (z R y \leftrightarrow x R y)$
47	46	rspcev	$⊢ (x \in Pred (R^{-1}, A, X) \land x R y) \to \exists z \in Pred (R^{-1}, A, X) z R y$
48	44 45 47	syl2anc	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A \land x R y) \to \exists z \in Pred (R^{-1}, A, X) z R y$
49	48	3expia	$⊢ ((φ \land (x \in A \land x R^{-1} X)) \land y \in A) \to (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)$
50	49	ralrimiva	$⊢ (φ \land (x \in A \land x R^{-1} X)) \to \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)$
51	50	expr	$⊢ (φ \land x \in A) \to (x R^{-1} X \to \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y))$
52	37 51	anim12d	$⊢ (φ \land x \in A) \to ((Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \land x R^{-1} X) \to (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)))$
53	52	ancomsd	$⊢ (φ \land x \in A) \to ((x R^{-1} X \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \to (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)))$
54	53	reximdva	$⊢ φ \to (\exists x \in A (x R^{-1} X \land Pred (R, Pred (R^{-1}, A, X), x) = \emptyset) \to \exists x \in A (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)))$
55	24 54	biimtrid	$⊢ φ \to (\exists x \in \{y \in A \| y R^{-1} X\} Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \to \exists x \in A (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)))$
56	22 55	sylbid	$⊢ φ \to (\exists x \in Pred (R^{-1}, A, X) Pred (R, Pred (R^{-1}, A, X), x) = \emptyset \to \exists x \in A (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y)))$
57	19 56	mpd	$⊢ φ \to \exists x \in A (\forall y \in Pred (R^{-1}, A, X) \neg y R x \land \forall y \in A (x R y \to \exists z \in Pred (R^{-1}, A, X) z R y))$

Metamath Proof Explorer

Theorem wsuclem

Proof