fr0

Description: Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993)

		Ref	Expression
	Assertion	fr0	$⊢ R Fr \emptyset$

Step	Hyp	Ref	Expression
1		dffr2	$⊢ R Fr \emptyset \leftrightarrow \forall x ((x \subseteq \emptyset \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$
2		ss0	$⊢ x \subseteq \emptyset \to x = \emptyset$
3	2	a1d	$⊢ x \subseteq \emptyset \to (\neg \exists y \in x \{z \in x \| z R y\} = \emptyset \to x = \emptyset)$
4	3	necon1ad	$⊢ x \subseteq \emptyset \to (x \neq \emptyset \to \exists y \in x \{z \in x \| z R y\} = \emptyset)$
5	4	imp	$⊢ (x \subseteq \emptyset \land x \neq \emptyset) \to \exists y \in x \{z \in x \| z R y\} = \emptyset$
6	1 5	mpgbir	$⊢ R Fr \emptyset$

Metamath Proof Explorer