Metamath Proof Explorer

Theorem dffr3

Description: Alternate definition of well-founded relation. Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 23-Apr-2004) (Revised by Mario Carneiro, 23-Jun-2015)

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		dffr2	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$
2		iniseg	$⊢ y \in V \to R^{-1} [\{y\}] = \{z \| z R y\}$
3	2	elv	$⊢ R^{-1} [\{y\}] = \{z \| z R y\}$
4	3	ineq2i	$⊢ x \cap R^{-1} [\{y\}] = x \cap \{z \| z R y\}$
5		dfrab3	$⊢ \{z \in x \| z R y\} = x \cap \{z \| z R y\}$
6	4 5	eqtr4i	$⊢ x \cap R^{-1} [\{y\}] = \{z \in x \| z R y\}$
7	6	eqeq1i	$⊢ x \cap R^{-1} [\{y\}] = \emptyset \leftrightarrow \{z \in x \| z R y\} = \emptyset$
8	7	rexbii	$⊢ \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset \leftrightarrow \exists y \in x \{z \in x \| z R y\} = \emptyset$
9	8	imbi2i	$⊢ ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$
10	9	albii	$⊢ \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$
11	1 10	bitr4i	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x x \cap R^{-1} [\{y\}] = \emptyset)$