This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frss

Description: Subset theorem for the well-founded predicate. Exercise 1 of TakeutiZaring p. 31. (Contributed by NM, 3-Apr-1994) (Proof shortened by Andrew Salmon, 25-Jul-2011)

		Ref	Expression
	Assertion	frss	$⊢ A \subseteq B \to (R Fr B \to R Fr A)$

Proof

Step	Hyp	Ref	Expression
1		sstr2	$⊢ x \subseteq A \to (A \subseteq B \to x \subseteq B)$
2	1	com12	$⊢ A \subseteq B \to (x \subseteq A \to x \subseteq B)$
3	2	anim1d	$⊢ A \subseteq B \to ((x \subseteq A \land x \neq \emptyset) \to (x \subseteq B \land x \neq \emptyset))$
4	3	imim1d	$⊢ A \subseteq B \to (((x \subseteq B \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \to ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y))$
5	4	alimdv	$⊢ A \subseteq B \to (\forall x ((x \subseteq B \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y) \to \forall x ((x \subseteq A \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y))$
6		df-fr	$⊢ R Fr B \leftrightarrow \forall x ((x \subseteq B \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z R y)$
7		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)$
8	5 6 7	3imtr4g	$⊢ A \subseteq B \to (R Fr B \to R Fr A)$