frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relationship. (Contributed by Scott Fenton, 11-Sep-2023)

		Ref	Expression
	Assertion	frrlem16	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall w \in TrPred (R, A, z) Pred (R, A, w) \subseteq TrPred (R, A, z)$

Step	Hyp	Ref	Expression
1		simplr	$⊢ (((R Fr A \land R Se A) \land z \in A) \land w \in TrPred (R, A, z)) \to z \in A$
2		simpllr	$⊢ (((R Fr A \land R Se A) \land z \in A) \land w \in TrPred (R, A, z)) \to R Se A$
3	1 2	jca	$⊢ (((R Fr A \land R Se A) \land z \in A) \land w \in TrPred (R, A, z)) \to (z \in A \land R Se A)$
4		simpr	$⊢ (((R Fr A \land R Se A) \land z \in A) \land w \in TrPred (R, A, z)) \to w \in TrPred (R, A, z)$
5		trpredtr	$⊢ (z \in A \land R Se A) \to (w \in TrPred (R, A, z) \to Pred (R, A, w) \subseteq TrPred (R, A, z))$
6	3 4 5	sylc	$⊢ (((R Fr A \land R Se A) \land z \in A) \land w \in TrPred (R, A, z)) \to Pred (R, A, w) \subseteq TrPred (R, A, z)$
7	6	ralrimiva	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall w \in TrPred (R, A, z) Pred (R, A, w) \subseteq TrPred (R, A, z)$

Metamath Proof Explorer