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 ↾}_{Pred (t++ ({R ↾}_{A}), A, z)}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} = ({F ↾}_{Pred (t++ ({R ↾}_{A}), 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		predres	$⊢ Pred (R, A, z) = Pred (({R ↾}_{A}), A, z)$
9		relres	$⊢ Rel ({R ↾}_{A})$
10		ssttrcl	$⊢ Rel ({R ↾}_{A}) \to {R ↾}_{A} \subseteq t++ ({R ↾}_{A})$
11		predrelss	$⊢ {R ↾}_{A} \subseteq t++ ({R ↾}_{A}) \to Pred (({R ↾}_{A}), A, z) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
12	9 10 11	mp2b	$⊢ Pred (({R ↾}_{A}), A, z) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
13	8 12	eqsstri	$⊢ Pred (R, A, z) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
14	13	a1i	$⊢ ((R Fr A \land R Se A) \land z \in A) \to Pred (R, A, z) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
15		frrlem16	$⊢ ((R Fr A \land R Se A) \land z \in A) \to \forall a \in Pred (t++ ({R ↾}_{A}), A, z) Pred (R, A, a) \subseteq Pred (t++ ({R ↾}_{A}), A, z)$
16		ttrclse	$⊢ R Se A \to t++ ({R ↾}_{A}) Se A$
17		setlikespec	$⊢ (z \in A \land t++ ({R ↾}_{A}) Se A) \to Pred (t++ ({R ↾}_{A}), A, z) \in V$
18	17	ancoms	$⊢ (t++ ({R ↾}_{A}) Se A \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, z) \in V$
19	16 18	sylan	$⊢ (R Se A \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, z) \in V$
20	19	adantll	$⊢ ((R Fr A \land R Se A) \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, z) \in V$
21		predss	$⊢ Pred (t++ ({R ↾}_{A}), A, z) \subseteq A$
22	21	a1i	$⊢ ((R Fr A \land R Se A) \land z \in A) \to Pred (t++ ({R ↾}_{A}), A, z) \subseteq A$
23		difss	$⊢ A ∖ dom F \subseteq A$
24		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$
25	23 24	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$
26	3 1 4 6 7 14 15 20 22 25	frrlem14	$⊢ (R Fr A \land R Se A) \to dom F = A$
27		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
28	5 26 27	sylanbrc	$⊢ (R Fr A \land R Se A) \to F Fn A$

Metamath Proof Explorer

Theorem frr1

Proof