wzel

Description: The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018) (Revised by AV, 10-Oct-2021)

		Ref	Expression
	Assertion	wzel	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to inf (A, A, R) \in A$

Proof

Step	Hyp	Ref	Expression
1		weso	$⊢ R We A \to R Or A$
2	1	3ad2ant1	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to R Or A$
3		simp1	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to R We A$
4		simp2	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to R Se A$
5		ssidd	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to A \subseteq A$
6		simp3	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to A \neq \emptyset$
7		tz6.26	$⊢ ((R We A \land R Se A) \land (A \subseteq A \land A \neq \emptyset)) \to \exists x \in A Pred (R, A, x) = \emptyset$
8	3 4 5 6 7	syl22anc	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to \exists x \in A Pred (R, A, x) = \emptyset$
9		vex	$⊢ y \in V$
10	9	elpred	$⊢ x \in V \to (y \in Pred (R, A, x) \leftrightarrow (y \in A \land y R x))$
11	10	elv	$⊢ y \in Pred (R, A, x) \leftrightarrow (y \in A \land y R x)$
12	11	notbii	$⊢ \neg y \in Pred (R, A, x) \leftrightarrow \neg (y \in A \land y R x)$
13		imnan	$⊢ (y \in A \to \neg y R x) \leftrightarrow \neg (y \in A \land y R x)$
14	12 13	bitr4i	$⊢ \neg y \in Pred (R, A, x) \leftrightarrow (y \in A \to \neg y R x)$
15		pm2.27	$⊢ y \in A \to ((y \in A \to \neg y R x) \to \neg y R x)$
16	15	ad2antll	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land (x \in A \land y \in A)) \to ((y \in A \to \neg y R x) \to \neg y R x)$
17		breq1	$⊢ z = x \to (z R y \leftrightarrow x R y)$
18	17	rspcev	$⊢ (x \in A \land x R y) \to \exists z \in A z R y$
19	18	ex	$⊢ x \in A \to (x R y \to \exists z \in A z R y)$
20	19	ad2antrl	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land (x \in A \land y \in A)) \to (x R y \to \exists z \in A z R y)$
21	16 20	jctird	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land (x \in A \land y \in A)) \to ((y \in A \to \neg y R x) \to (\neg y R x \land (x R y \to \exists z \in A z R y)))$
22	14 21	biimtrid	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land (x \in A \land y \in A)) \to (\neg y \in Pred (R, A, x) \to (\neg y R x \land (x R y \to \exists z \in A z R y)))$
23	22	expr	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land x \in A) \to (y \in A \to (\neg y \in Pred (R, A, x) \to (\neg y R x \land (x R y \to \exists z \in A z R y))))$
24	23	com23	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land x \in A) \to (\neg y \in Pred (R, A, x) \to (y \in A \to (\neg y R x \land (x R y \to \exists z \in A z R y))))$
25	24	alimdv	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land x \in A) \to (\forall y \neg y \in Pred (R, A, x) \to \forall y (y \in A \to (\neg y R x \land (x R y \to \exists z \in A z R y))))$
26		eq0	$⊢ Pred (R, A, x) = \emptyset \leftrightarrow \forall y \neg y \in Pred (R, A, x)$
27		r19.26	$⊢ \forall y \in A (\neg y R x \land (x R y \to \exists z \in A z R y)) \leftrightarrow (\forall y \in A \neg y R x \land \forall y \in A (x R y \to \exists z \in A z R y))$
28		df-ral	$⊢ \forall y \in A (\neg y R x \land (x R y \to \exists z \in A z R y)) \leftrightarrow \forall y (y \in A \to (\neg y R x \land (x R y \to \exists z \in A z R y)))$
29	27 28	bitr3i	$⊢ (\forall y \in A \neg y R x \land \forall y \in A (x R y \to \exists z \in A z R y)) \leftrightarrow \forall y (y \in A \to (\neg y R x \land (x R y \to \exists z \in A z R y)))$
30	25 26 29	3imtr4g	$⊢ ((R We A \land R Se A \land A \neq \emptyset) \land x \in A) \to (Pred (R, A, x) = \emptyset \to (\forall y \in A \neg y R x \land \forall y \in A (x R y \to \exists z \in A z R y)))$
31	30	reximdva	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to (\exists x \in A Pred (R, A, x) = \emptyset \to \exists x \in A (\forall y \in A \neg y R x \land \forall y \in A (x R y \to \exists z \in A z R y)))$
32	8 31	mpd	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to \exists x \in A (\forall y \in A \neg y R x \land \forall y \in A (x R y \to \exists z \in A z R y))$
33	2 32	infcl	$⊢ (R We A \land R Se A \land A \neq \emptyset) \to inf (A, A, R) \in A$

Metamath Proof Explorer

Theorem wzel

Proof