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) Avoid ax-10 , ax-11 , ax-12 , but use ax-8 . (Revised by Gino Giotto, 3-Oct-2024)

		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 w \in x \neg w R y)$
2		breq1	$⊢ z = w \to (z R y \leftrightarrow w R y)$
3	2	rabeq0w	$⊢ \{z \in x \| z R y\} = \emptyset \leftrightarrow \forall w \in x \neg w R y$
4	3	rexbii	$⊢ \exists y \in x \{z \in x \| z R y\} = \emptyset \leftrightarrow \exists y \in x \forall w \in x \neg w R y$
5	4	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 w \in x \neg w R y)$
6	5	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 w \in x \neg w R y)$
7	1 6	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)$

Metamath Proof Explorer

Theorem dffr2

Proof