fpr2

Description: Law of well-founded recursion over a partial order, part two. Now we establish the value of F within A . (Contributed by Scott Fenton, 11-Sep-2023)

		Ref	Expression
	Hypothesis	fprr.1	$⊢ F = frecs (R, A, G)$
	Assertion	fpr2	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$

Proof

Step	Hyp	Ref	Expression
1		fprr.1	$⊢ F = frecs (R, A, G)$
2	1	fpr1	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$
3	2	fndmd	$⊢ (R Fr A \land R Po A \land R Se A) \to dom F = A$
4	3	eleq2d	$⊢ (R Fr A \land R Po A \land R Se A) \to (X \in dom F \leftrightarrow X \in A)$
5	4	biimpar	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to X \in dom F$
6		fveq2	$⊢ y = X \to F (y) = F (X)$
7		id	$⊢ y = X \to y = X$
8		predeq3	$⊢ y = X \to Pred (R, A, y) = Pred (R, A, X)$
9	8	reseq2d	$⊢ y = X \to {F ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, X)}$
10	7 9	oveq12d	$⊢ y = X \to y G ({F ↾}_{Pred (R, A, y)}) = X G ({F ↾}_{Pred (R, A, X)})$
11	6 10	eqeq12d	$⊢ y = X \to (F (y) = y G ({F ↾}_{Pred (R, A, y)}) \leftrightarrow F (X) = X G ({F ↾}_{Pred (R, A, X)}))$
12	11	imbi2d	$⊢ y = X \to (((R Fr A \land R Po A \land R Se A) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})) \leftrightarrow ((R Fr A \land R Po A \land R Se A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})))$
13		eqid	$⊢ \{a \| \exists b (a Fn b \land (b \subseteq A \land \forall c \in b Pred (R, A, c) \subseteq b) \land \forall c \in b a (c) = c G ({a ↾}_{Pred (R, A, c)}))\} = \{a \| \exists b (a Fn b \land (b \subseteq A \land \forall c \in b Pred (R, A, c) \subseteq b) \land \forall c \in b a (c) = c G ({a ↾}_{Pred (R, A, c)}))\}$
14	13	frrlem1	$⊢ \{a \| \exists b (a Fn b \land (b \subseteq A \land \forall c \in b Pred (R, A, c) \subseteq b) \land \forall c \in b a (c) = c G ({a ↾}_{Pred (R, A, c)}))\} = \{f \| \exists x (f Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x f (y) = y G ({f ↾}_{Pred (R, A, y)}))\}$
15	14 1	fprlem1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in \{a \| \exists b (a Fn b \land (b \subseteq A \land \forall c \in b Pred (R, A, c) \subseteq b) \land \forall c \in b a (c) = c G ({a ↾}_{Pred (R, A, c)}))\} \land h \in \{a \| \exists b (a Fn b \land (b \subseteq A \land \forall c \in b Pred (R, A, c) \subseteq b) \land \forall c \in b a (c) = c G ({a ↾}_{Pred (R, A, c)}))\})) \to ((x g u \land x h v) \to u = v)$
16	14 1 15	frrlem10	$⊢ ((R Fr A \land R Po A \land R Se A) \land y \in dom F) \to F (y) = y G ({F ↾}_{Pred (R, A, y)})$
17	16	expcom	$⊢ y \in dom F \to ((R Fr A \land R Po A \land R Se A) \to F (y) = y G ({F ↾}_{Pred (R, A, y)}))$
18	12 17	vtoclga	$⊢ X \in dom F \to ((R Fr A \land R Po A \land R Se A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)}))$
19	18	impcom	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in dom F) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$
20	5 19	syldan	$⊢ ((R Fr A \land R Po A \land R Se A) \land X \in A) \to F (X) = X G ({F ↾}_{Pred (R, A, X)})$

Metamath Proof Explorer

Theorem fpr2

Proof