Metamath Proof Explorer

Theorem dffr2

Description: Alternate definition of well-founded relation. Similar to Definition 6.21 of TakeutiZaring p. 30. (Contributed by NM, 17-Feb-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Proof shortened by Mario Carneiro, 23-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		df-fr	$⊢ R Fr A \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
2		rabeq0	$⊢ \{z \in x \| z R y\} = \emptyset \leftrightarrow \forall z \in x \neg z R y$
3	2	rexbii	$⊢ \exists y \in x \{z \in x \| z R y\} = \emptyset \leftrightarrow \exists y \in x \forall z \in x \neg z R y$
4	3	imbi2i	$⊢ ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset) \leftrightarrow ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
5	4	albii	$⊢ \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset) \leftrightarrow \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
6	1 5	bitr4i	$⊢ 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)$