fpr1

Description: Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023)

		Ref	Expression
	Hypothesis	fprr.1	$⊢ F = frecs (R, A, G)$
	Assertion	fpr1	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$

Proof

Step	Hyp	Ref	Expression
1		fprr.1	$⊢ F = frecs (R, A, G)$
2		eqid	$⊢ \{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)}))\} = \{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)}))\}$
3	2	frrlem1	$⊢ \{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)}))\} = \{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)}))\}$
4	3 1	fprlem1	$⊢ ((R Fr A \land R Po A \land R Se A) \land (g \in \{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)}))\} \land h \in \{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)}))\})) \to ((b g u \land b h v) \to u = v)$
5	3 1 4	frrlem9	$⊢ (R Fr A \land R Po A \land R Se A) \to Fun F$
6		eqid	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} = ({F ↾}_{Pred (R, A, z)}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
7		simp1	$⊢ (R Fr A \land R Po A \land R Se A) \to R Fr A$
8		ssidd	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to Pred (R, A, z) \subseteq Pred (R, A, z)$
9		fprlem2	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to \forall y \in Pred (R, A, z) Pred (R, A, y) \subseteq Pred (R, A, z)$
10		setlikespec	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \in V$
11	10	ancoms	$⊢ (R Se A \land z \in A) \to Pred (R, A, z) \in V$
12	11	3ad2antl3	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to Pred (R, A, z) \in V$
13		predss	$⊢ Pred (R, A, z) \subseteq A$
14	13	a1i	$⊢ ((R Fr A \land R Po A \land R Se A) \land z \in A) \to Pred (R, A, z) \subseteq A$
15		difssd	$⊢ ((R Fr A \land R Po A \land R Se A) \land A ∖ dom F \neq \emptyset) \to A ∖ dom F \subseteq A$
16		simpr	$⊢ ((R Fr A \land R Po A \land R Se A) \land A ∖ dom F \neq \emptyset) \to A ∖ dom F \neq \emptyset$
17	15 16	jca	$⊢ ((R Fr A \land R Po A \land R Se A) \land A ∖ dom F \neq \emptyset) \to (A ∖ dom F \subseteq A \land A ∖ dom F \neq \emptyset)$
18		frpomin2	$⊢ ((R Fr A \land R Po A \land R Se A) \land (A ∖ dom F \subseteq A \land A ∖ dom F \neq \emptyset)) \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
19	17 18	syldan	$⊢ ((R Fr A \land R Po A \land R Se A) \land A ∖ dom F \neq \emptyset) \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
20	3 1 4 6 7 8 9 12 14 19	frrlem14	$⊢ (R Fr A \land R Po A \land R Se A) \to dom F = A$
21		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
22	5 20 21	sylanbrc	$⊢ (R Fr A \land R Po A \land R Se A) \to F Fn A$

Metamath Proof Explorer

Theorem fpr1

Proof