frrlem11

Description: Lemma for 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 ordering or Infinity. To begin with, we establish the functionhood 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		funres	$⊢ Fun F \to Fun ({F ↾}_{S})$
7	5 6	syl	$⊢ φ \to Fun ({F ↾}_{S})$
8		dmres	$⊢ dom ({F ↾}_{S}) = S \cap dom F$
9		df-fn	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow (Fun ({F ↾}_{S}) \land dom ({F ↾}_{S}) = S \cap dom F)$
10	8 9	mpbiran2	$⊢ ({F ↾}_{S}) Fn (S \cap dom F) \leftrightarrow Fun ({F ↾}_{S})$
11	7 10	sylibr	$⊢ φ \to ({F ↾}_{S}) Fn (S \cap dom F)$
12		vex	$⊢ z \in V$
13		ovex	$⊢ z G ({F ↾}_{Pred (R, A, z)}) \in V$
14	12 13	fnsn	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\}$
15	11 14	jctir	$⊢ φ \to (({F ↾}_{S}) Fn (S \cap dom F) \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} Fn \{z\})$
16		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
17		elinel2	$⊢ z \in (S \cap dom F) \to z \in dom F$
18	16 17	nsyl	$⊢ z \in (A ∖ dom F) \to \neg z \in (S \cap dom F)$
19		disjsn	$⊢ (S \cap dom F) \cap \{z\} = \emptyset \leftrightarrow \neg z \in (S \cap dom F)$
20	18 19	sylibr	$⊢ z \in (A ∖ dom F) \to (S \cap dom F) \cap \{z\} = \emptyset$
21		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\})$
22	15 20 21	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\})$
23	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\})$
24	22 23	sylibr	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$

Metamath Proof Explorer

Theorem frrlem11

Proof