frr1

Description: Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 , fpr2 , and fpr3 , which requires using the axiom of infinity (Contributed by Scott Fenton, 11-Sep-2023)

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

Proof

Step	Hyp	Ref	Expression
1		frr.1	$⊢ F = frecs (R, A, G)$
2		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)}))\}$
3	2	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)}))\}$
4	3 1	frrlem15	$⊢ ((R Fr 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)$
5	3 1 4	frrlem9	$⊢ (R Fr A \land R Se A) \to Fun F$
6		eqid	$⊢ ({F ↾}_{TrPred (R, A, z)}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} = ({F ↾}_{TrPred (R, A, z)}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
7		simpl	$⊢ (R Fr A \land R Se A) \to R Fr A$
8		setlikespec	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \in V$
9	8	ancoms	$⊢ (R Se A \land z \in A) \to Pred (R, A, z) \in V$
10	9	adantll	$⊢ ((R Fr A \land R Se A) \land z \in A) \to Pred (R, A, z) \in V$
11		trpredpred	$⊢ Pred (R, A, z) \in V \to Pred (R, A, z) \subseteq TrPred (R, A, z)$
12	10 11	syl	$⊢ ((R Fr A \land R Se A) \land z \in A) \to Pred (R, A, z) \subseteq TrPred (R, A, z)$
13		frrlem16	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall a \in TrPred (R, A, z) Pred (R, A, a) \subseteq TrPred (R, A, z)$
14		trpredex	$⊢ TrPred (R, A, z) \in V$
15	14	a1i	$⊢ ((R Fr A \land R Se A) \land z \in A) \to TrPred (R, A, z) \in V$
16		trpredss	$⊢ Pred (R, A, z) \in V \to TrPred (R, A, z) \subseteq A$
17	10 16	syl	$⊢ ((R Fr A \land R Se A) \land z \in A) \to TrPred (R, A, z) \subseteq A$
18		difss	$⊢ A ∖ dom F \subseteq A$
19		frmin	$⊢ ((R Fr 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$
20	18 19	mpanr1	$⊢ ((R Fr 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$
21	3 1 4 6 7 12 13 15 17 20	frrlem14	$⊢ (R Fr A \land R Se A) \to dom F = A$
22		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
23	5 21 22	sylanbrc	$⊢ (R Fr A \land R Se A) \to F Fn A$

Metamath Proof Explorer

Theorem frr1

Proof