sswf

Description: A subset of a well-founded set is well-founded. (Contributed by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	sswf	$⊢ (A \in ⋃ R_{1} [On] \land B \subseteq A) \to B \in ⋃ R_{1} [On]$

Step	Hyp	Ref	Expression
1		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
2		r1sscl	$⊢ (A \in R_{1} (suc rank (A)) \land B \subseteq A) \to B \in R_{1} (suc rank (A))$
3	1 2	sylan	$⊢ (A \in ⋃ R_{1} [On] \land B \subseteq A) \to B \in R_{1} (suc rank (A))$
4		r1elwf	$⊢ B \in R_{1} (suc rank (A)) \to B \in ⋃ R_{1} [On]$
5	3 4	syl	$⊢ (A \in ⋃ R_{1} [On] \land B \subseteq A) \to B \in ⋃ R_{1} [On]$

Metamath Proof Explorer