frrlem11

Description: Lemma for well-founded recursion. For the next several theorems we will be aiming to prove that dom F = A . To do this, we set up a function C that supposedly contains an element of A that is not in dom F and we show that the element must be in dom F . Our choice of what to restrict F to depends on if we assume partial orders or the axiom of infinity. To begin with, we establish the functionality of C . (Contributed by Scott Fenton, 7-Dec-2022)

	Ref	Expression
Hypotheses	frrlem11.1	$⊢ B = \{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)}))\}$
	frrlem11.2	$⊢ F = frecs (R, A, G)$
	frrlem11.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
	frrlem11.4	$⊢ C = ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
Assertion	frrlem11	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$

Proof

Step	Hyp	Ref	Expression
1		frrlem11.1	$⊢ B = \{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)}))\}$
2		frrlem11.2	$⊢ F = frecs (R, A, G)$
3		frrlem11.3	$⊢ (φ \land (g \in B \land h \in B)) \to ((x g u \land x h v) \to u = v)$
4		frrlem11.4	$⊢ C = ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
5	1 2 3	frrlem9	$⊢ φ \to Fun F$
6	5	funresd	$⊢ φ \to Fun ({F ↾}_{S})$
7		dmres	$⊢ dom ({F ↾}_{S}) = S \cap dom F$
8		df-fn	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow (Fun ({F ↾}_{S}) \land dom ({F ↾}_{S}) = S \cap dom F)$
9	7 8	mpbiran2	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow Fun ({F ↾}_{S})$
10	6 9	sylibr	$⊢ φ \to ({F ↾}_{S}) Fn (S \cap dom F)$
11		vex	$⊢ z \in V$
12		ovex	$⊢ z G ({F ↾}_{Pred (R, A, z)}) \in V$
13	11 12	fnsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
14	10 13	jctir	$⊢ φ \to (({F ↾}_{S}) Fn (S \cap dom F) \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\})$
15		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
16		elinel2	$⊢ z \in (S \cap dom F) \to z \in dom F$
17	15 16	nsyl	$⊢ z \in (A ∖ dom F) \to \neg z \in (S \cap dom F)$
18		disjsn	$⊢ (S \cap dom F) \cap \{z\} = \emptyset \leftrightarrow \neg z \in (S \cap dom F)$
19	17 18	sylibr	$⊢ z \in (A ∖ dom F) \to (S \cap dom F) \cap \{z\} = \emptyset$
20		fnun	$⊢ ((({F ↾}_{S}) Fn (S \cap dom F) \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}) \land (S \cap dom F) \cap \{z\} = \emptyset) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) Fn ((S \cap dom F) \cup \{z\})$
21	14 19 20	syl2an	$⊢ (φ \land z \in (A ∖ dom F)) \to (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) Fn ((S \cap dom F) \cup \{z\})$
22	4	fneq1i	$⊢ C Fn ((S \cap dom F) \cup \{z\}) \leftrightarrow (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) Fn ((S \cap dom F) \cup \{z\})$
23	21 22	sylibr	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$

Metamath Proof Explorer

Theorem frrlem11

Proof