Theorem fr0

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

	Ref	Expression
Assertion	fr0	$$⊢R\mathrm{Fr}\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		dffr2	$$⊢R\mathrm{Fr}\varnothing \leftrightarrow \forall x\left(\left(x\subseteq \varnothing \wedge x\ne \varnothing \right)\to \exists y\in x\left\{z\in x|zRy\right\}=\varnothing \right)$$
2		ss0	$$⊢x\subseteq \varnothing \to x=\varnothing$$
3	2	a1d	$$⊢x\subseteq \varnothing \to \left(\neg \exists y\in x\left\{z\in x|zRy\right\}=\varnothing \to x=\varnothing \right)$$
4	3	necon1ad	$$⊢x\subseteq \varnothing \to \left(x\ne \varnothing \to \exists y\in x\left\{z\in x|zRy\right\}=\varnothing \right)$$
5	4	imp	$$⊢\left(x\subseteq \varnothing \wedge x\ne \varnothing \right)\to \exists y\in x\left\{z\in x|zRy\right\}=\varnothing$$
6	1 5	mpgbir	$$⊢R\mathrm{Fr}\varnothing$$