wfrlem13

Description: Lemma for well-founded recursion. From here through wfrlem16 , 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. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

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

Proof

Step	Hyp	Ref	Expression
1		wfrlem13.1	$⊢ R We A$
2		wfrlem13.2	$⊢ R Se A$
3		wfrlem13.3	$⊢ F = wrecs (R, A, G)$
4		wfrlem13.4	$⊢ C = F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
5	1 2 3	wfrfun	$⊢ 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	syl5eq	$⊢ 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 wfrlem13

Proof