wfrlem16

Description: Lemma for well-founded recursion. If z is R minimal in ( A \ dom F ) , then C is acceptable and thus a subset of F , but dom C is bigger than dom F . Thus, z cannot be minimal, so ( A \ dom F ) must be empty, and (due to wfrdmss ), dom F = A . (Contributed by Scott Fenton, 21-Apr-2011)

	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	wfrlem16	$⊢ dom F = A$

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	3	wfrdmss	$⊢ dom F \subseteq A$
6		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
7		ssun2	$⊢ \{z\} \subseteq dom F \cup \{z\}$
8		vsnid	$⊢ z \in \{z\}$
9	7 8	sselii	$⊢ z \in (dom F \cup \{z\})$
10	4	dmeqi	$⊢ dom C = dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
11		dmun	$⊢ dom (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom F \cup dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
12		fvex	$⊢ G ({F ↾}_{Pred (R, A, z)}) \in V$
13	12	dmsnop	$⊢ dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = \{z\}$
14	13	uneq2i	$⊢ dom F \cup dom \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} = dom F \cup \{z\}$
15	10 11 14	3eqtri	$⊢ dom C = dom F \cup \{z\}$
16	9 15	eleqtrri	$⊢ z \in dom C$
17	1 2 3 4	wfrlem15	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to C \in \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
18		elssuni	$⊢ C \in \{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) = G ({f ↾}_{Pred (R, A, y)}))\} \to C \subseteq ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
19	17 18	syl	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to C \subseteq ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
20		df-wrecs	$⊢ wrecs (R, A, G) = ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
21	3 20	eqtri	$⊢ F = ⋃ \{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) = G ({f ↾}_{Pred (R, A, y)}))\}$
22	19 21	sseqtrrdi	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to C \subseteq F$
23		dmss	$⊢ C \subseteq F \to dom C \subseteq dom F$
24	22 23	syl	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to dom C \subseteq dom F$
25	24	sseld	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (z \in dom C \to z \in dom F)$
26	16 25	mpi	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to z \in dom F$
27	6 26	mtand	$⊢ z \in (A ∖ dom F) \to \neg Pred (R, (A ∖ dom F), z) = \emptyset$
28	27	nrex	$⊢ \neg \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
29		df-ne	$⊢ A ∖ dom F \neq \emptyset \leftrightarrow \neg A ∖ dom F = \emptyset$
30		difss	$⊢ A ∖ dom F \subseteq A$
31	1 2	tz6.26i	$⊢ (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$
32	30 31	mpan	$⊢ A ∖ dom F \neq \emptyset \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
33	29 32	sylbir	$⊢ \neg A ∖ dom F = \emptyset \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
34	28 33	mt3	$⊢ A ∖ dom F = \emptyset$
35		ssdif0	$⊢ A \subseteq dom F \leftrightarrow A ∖ dom F = \emptyset$
36	34 35	mpbir	$⊢ A \subseteq dom F$
37	5 36	eqssi	$⊢ dom F = A$

Metamath Proof Explorer

Theorem wfrlem16

Proof