wfrlem13OLD

Description: Lemma for well-ordered recursion. From here through wfrlem16OLD , we aim to prove that dom F = A . We do this by supposing that there is an element z of A that is not in dom F . We then define C by extending dom F with the appropriate value at z . We then show that z cannot be an R minimal element of ( A \ dom F ) , meaning that ( A \ dom F ) must be empty, so dom F = A . Here, we show that C is a function extending the domain of F by one. Obsolete as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrlem13OLD.1	$⊢ R We A$
	wfrlem13OLD.2	$⊢ R Se A$
	wfrlem13OLD.3	$⊢ F = wrecs (R, A, G)$
	wfrlem13OLD.4	$⊢ C = F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
Assertion	wfrlem13OLD	$⊢ z \in (A ∖ dom F) \to C Fn (dom F \cup \{z\})$

Proof

Step	Hyp	Ref	Expression
1		wfrlem13OLD.1	$⊢ R We A$
2		wfrlem13OLD.2	$⊢ R Se A$
3		wfrlem13OLD.3	$⊢ F = wrecs (R, A, G)$
4		wfrlem13OLD.4	$⊢ C = F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
5	1 2 3	wfrfunOLD	$⊢ Fun F$
6		vex	$⊢ z \in V$
7		fvex	$⊢ G ({F ↾}_{Pred (R, A, z)}) \in V$
8	6 7	funsn	$⊢ Fun \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
9	5 8	pm3.2i	$⊢ (Fun F \land Fun \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
10	7	dmsnop	$⊢ dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = \{z\}$
11	10	ineq2i	$⊢ dom F \cap dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = dom F \cap \{z\}$
12		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
13		disjsn	$⊢ dom F \cap \{z\} = \emptyset \leftrightarrow \neg z \in dom F$
14	12 13	sylibr	$⊢ z \in (A ∖ dom F) \to dom F \cap \{z\} = \emptyset$
15	11 14	eqtrid	$⊢ z \in (A ∖ dom F) \to dom F \cap dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = \emptyset$
16		funun	$⊢ ((Fun F \land Fun \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) \land dom F \cap dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = \emptyset) \to Fun (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
17	9 15 16	sylancr	$⊢ z \in (A ∖ dom F) \to Fun (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
18		dmun	$⊢ dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom F \cup dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
19	10	uneq2i	$⊢ dom F \cup dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = dom F \cup \{z\}$
20	18 19	eqtri	$⊢ dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom F \cup \{z\}$
21	4	fneq1i	$⊢ C Fn (dom F \cup \{z\}) \leftrightarrow (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) Fn (dom F \cup \{z\})$
22		df-fn	$⊢ (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) Fn (dom F \cup \{z\}) \leftrightarrow (Fun (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) \land dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom F \cup \{z\})$
23	21 22	bitri	$⊢ C Fn (dom F \cup \{z\}) \leftrightarrow (Fun (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) \land dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom F \cup \{z\})$
24	17 20 23	sylanblrc	$⊢ z \in (A ∖ dom F) \to C Fn (dom F \cup \{z\})$

Metamath Proof Explorer

Theorem wfrlem13OLD

Proof