fprlem2

Description: Lemma for well-founded recursion with a partial order. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ w \in V$
2	1	elpred	$⊢ z \in V \to (w \in Pred (R, A, z) \leftrightarrow (w \in A \land w R z))$
3	2	elv	$⊢ w \in Pred (R, A, z) \leftrightarrow (w \in A \land w R z)$
4		simprl	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to x \in A$
5		simpll2	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \to R Po A$
6	5	adantr	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to R Po A$
7		simprl	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \to w \in A$
8	7	adantr	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to w \in A$
9		simpllr	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to z \in A$
10	4 8 9	3jca	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to (x \in A \land w \in A \land z \in A)$
11	6 10	jca	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to (R Po A \land (x \in A \land w \in A \land z \in A))$
12		simprr	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to x R w$
13		simplrr	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to w R z$
14	12 13	jca	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to (x R w \land w R z)$
15		potr	$⊢ (R Po A \land (x \in A \land w \in A \land z \in A)) \to ((x R w \land w R z) \to x R z)$
16	11 14 15	sylc	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to x R z$
17	4 16	jca	$⊢ ((((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \land (x \in A \land x R w)) \to (x \in A \land x R z)$
18	17	ex	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \to ((x \in A \land x R w) \to (x \in A \land x R z))$
19		vex	$⊢ x \in V$
20	19	elpred	$⊢ w \in V \to (x \in Pred (R, A, w) \leftrightarrow (x \in A \land x R w))$
21	20	elv	$⊢ x \in Pred (R, A, w) \leftrightarrow (x \in A \land x R w)$
22	19	elpred	$⊢ z \in V \to (x \in Pred (R, A, z) \leftrightarrow (x \in A \land x R z))$
23	22	elv	$⊢ x \in Pred (R, A, z) \leftrightarrow (x \in A \land x R z)$
24	18 21 23	3imtr4g	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \to (x \in Pred (R, A, w) \to x \in Pred (R, A, z))$
25	24	ssrdv	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land (w \in A \land w R z)) \to Pred (R, A, w) \subseteq Pred (R, A, z)$
26	3 25	sylan2b	$⊢ (((R Fr A \land R Po A \land R Se A) \land z \in A) \land w \in Pred (R, A, z)) \to Pred (R, A, w) \subseteq Pred (R, A, z)$
27	26	ralrimiva	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to \forall w \in Pred (R, A, z) Pred (R, A, w) \subseteq Pred (R, A, z)$

Metamath Proof Explorer

Theorem fprlem2

Proof