frrlem16

Description: Lemma for general well-founded recursion. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023) Revised notion of transitive closure. (Revised by Scott Fenton, 1-Dec-2024)

		Ref	Expression
	Assertion	frrlem16	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall w \in Pred (t++ ({R ↾}_{A}), A, z) Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$

Proof

Step	Hyp	Ref	Expression
1		predres	$⊢ Pred (R, A, w) = Pred (({R ↾}_{A}), A, w)$
2		relres	$⊢ Rel ({R ↾}_{A})$
3		ssttrcl	$⊢ Rel ({R ↾}_{A}) \to {R ↾}_{A} \subseteq t++ ({R ↾}_{A})$
4	2 3	ax-mp	$⊢ {R ↾}_{A} \subseteq t++ ({R ↾}_{A})$
5		predrelss	$⊢ {R ↾}_{A} \subseteq t++ ({R ↾}_{A}) \to Pred (({R ↾}_{A}), A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, w)$
6	4 5	ax-mp	$⊢ Pred (({R ↾}_{A}), A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, w)$
7	1 6	eqsstri	$⊢ Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, w)$
8		inss1	$⊢ t++ ({R ↾}_{A}) \cap (A \times A) \subseteq t++ ({R ↾}_{A})$
9		coss1	$⊢ t++ ({R ↾}_{A}) \cap (A \times A) \subseteq t++ ({R ↾}_{A}) \to (t++ ({R ↾}_{A}) \cap (A \times A)) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \circ (t++ ({R ↾}_{A}) \cap (A \times A))$
10	8 9	ax-mp	$⊢ (t++ ({R ↾}_{A}) \cap (A \times A)) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \circ (t++ ({R ↾}_{A}) \cap (A \times A))$
11		coss2	$⊢ t++ ({R ↾}_{A}) \cap (A \times A) \subseteq t++ ({R ↾}_{A}) \to t++ ({R ↾}_{A}) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \circ t++ ({R ↾}_{A})$
12	8 11	ax-mp	$⊢ t++ ({R ↾}_{A}) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \circ t++ ({R ↾}_{A})$
13	10 12	sstri	$⊢ (t++ ({R ↾}_{A}) \cap (A \times A)) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \circ t++ ({R ↾}_{A})$
14		ttrcltr	$⊢ t++ ({R ↾}_{A}) \circ t++ ({R ↾}_{A}) \subseteq t++ ({R ↾}_{A})$
15	13 14	sstri	$⊢ (t++ ({R ↾}_{A}) \cap (A \times A)) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A})$
16		predtrss	$⊢ ((t++ ({R ↾}_{A}) \cap (A \times A)) \circ (t++ ({R ↾}_{A}) \cap (A \times A)) \subseteq t++ ({R ↾}_{A}) \land w \in Pred (t++ ({R ↾}_{A}), A, z) \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
17	15 16	mp3an1	$⊢ (w \in Pred (t++ ({R ↾}_{A}), A, z) \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
18	7 17	sstrid	$⊢ (w \in Pred (t++ ({R ↾}_{A}), A, z) \land z \in A) \to Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
19	18	ancoms	$⊢ (z \in A \land w \in Pred (t++ ({R ↾}_{A}), A, z)) \to Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
20	19	ralrimiva	$⊢ z \in A \to \forall w \in Pred (t++ ({R ↾}_{A}), A, z) Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
21	20	adantl	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall w \in Pred (t++ ({R ↾}_{A}), A, z) Pred (R, A, w) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$

Metamath Proof Explorer

Theorem frrlem16

Proof