dffr4

Description: Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011)

		Ref	Expression
	Assertion	dffr4	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x Pred (R, x, y) = \emptyset)$

Step	Hyp	Ref	Expression
1		dffr3	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
2		df-pred	$⊢ Pred (R, x, y) = x \cap R^{-1} [\{y\}]$
3	2	eqeq1i	$⊢ Pred (R, x, y) = \emptyset \leftrightarrow x \cap R^{-1} [\{y\}] = \emptyset$
4	3	rexbii	$⊢ \exists y \in x Pred (R, x, y) = \emptyset \leftrightarrow \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset$
5	4	imbi2i	$⊢ ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x Pred (R, x, y) = \emptyset) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
6	5	albii	$⊢ \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x Pred (R, x, y) = \emptyset) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$
7	1 6	bitr4i	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x Pred (R, x, y) = \emptyset)$

Metamath Proof Explorer