frrlem14

Description: Lemma for well-founded recursion. Finally, we tie all these threads together and show that dom F = A when given the right S . Specifically, we prove that there can be no R -minimal element of ( A \ dom F ) . (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)})⟩\}$
	frrlem12.5	$⊢ φ \to R Fr A$
	frrlem12.6	$⊢ (φ \land z \in A) \to Pred (R, A, z) \subseteq S$
	frrlem12.7	$⊢ (φ \land z \in A) \to \forall w \in S Pred (R, A, w) \subseteq S$
	frrlem13.8	$⊢ (φ \land z \in A) \to S \in V$
	frrlem13.9	$⊢ (φ \land z \in A) \to S \subseteq A$
	frrlem14.10	$⊢ (φ \land A ∖ dom F \neq \emptyset) \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
Assertion	frrlem14	$⊢ φ \to dom F = A$

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		frrlem12.5	$⊢ φ \to R Fr A$
6		frrlem12.6	$⊢ (φ \land z \in A) \to Pred (R, A, z) \subseteq S$
7		frrlem12.7	$⊢ (φ \land z \in A) \to \forall w \in S Pred (R, A, w) \subseteq S$
8		frrlem13.8	$⊢ (φ \land z \in A) \to S \in V$
9		frrlem13.9	$⊢ (φ \land z \in A) \to S \subseteq A$
10		frrlem14.10	$⊢ (φ \land A ∖ dom F \neq \emptyset) \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
11	1 2	frrlem7	$⊢ dom F \subseteq A$
12	11	a1i	$⊢ φ \to dom F \subseteq A$
13		eldifn	$⊢ z \in (A ∖ dom F) \to \neg z \in dom F$
14	13	adantl	$⊢ (φ \land z \in (A ∖ dom F)) \to \neg z \in dom F$
15	1 2 3 4 5 6 7 8 9	frrlem13	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \in B$
16		elssuni	$⊢ C \in B \to C \subseteq ⋃ B$
17	15 16	syl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \subseteq ⋃ B$
18	1 2	frrlem5	$⊢ F = ⋃ B$
19	17 18	sseqtrrdi	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \subseteq F$
20		dmss	$⊢ C \subseteq F \to dom C \subseteq dom F$
21	19 20	syl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to dom C \subseteq dom F$
22		ssun2	$⊢ \{z\} \subseteq dom ({F ↾}_{S}) \cup \{z\}$
23		vsnid	$⊢ z \in \{z\}$
24	22 23	sselii	$⊢ z \in (dom ({F ↾}_{S}) \cup \{z\})$
25	4	dmeqi	$⊢ dom C = dom (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\})$
26		dmun	$⊢ dom (({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}) = dom ({F ↾}_{S}) \cup dom \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\}$
27		ovex	$⊢ z G ({F ↾}_{Pred (R, A, z)}) \in V$
28	27	dmsnop	$⊢ dom \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} = \{z\}$
29	28	uneq2i	$⊢ dom ({F ↾}_{S}) \cup dom \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} = dom ({F ↾}_{S}) \cup \{z\}$
30	25 26 29	3eqtri	$⊢ dom C = dom ({F ↾}_{S}) \cup \{z\}$
31	24 30	eleqtrri	$⊢ z \in dom C$
32	31	a1i	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to z \in dom C$
33	21 32	sseldd	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to z \in dom F$
34	33	expr	$⊢ (φ \land z \in (A ∖ dom F)) \to (Pred (R, (A ∖ dom F), z) = \emptyset \to z \in dom F)$
35	14 34	mtod	$⊢ (φ \land z \in (A ∖ dom F)) \to \neg Pred (R, (A ∖ dom F), z) = \emptyset$
36	35	nrexdv	$⊢ φ \to \neg \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
37		df-ne	$⊢ A ∖ dom F \neq \emptyset \leftrightarrow \neg A ∖ dom F = \emptyset$
38	37 10	sylan2br	$⊢ (φ \land \neg A ∖ dom F = \emptyset) \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset$
39	38	ex	$⊢ φ \to (\neg A ∖ dom F = \emptyset \to \exists z \in (A ∖ dom F) Pred (R, (A ∖ dom F), z) = \emptyset)$
40	36 39	mt3d	$⊢ φ \to A ∖ dom F = \emptyset$
41		ssdif0	$⊢ A \subseteq dom F \leftrightarrow A ∖ dom F = \emptyset$
42	40 41	sylibr	$⊢ φ \to A \subseteq dom F$
43	12 42	eqssd	$⊢ φ \to dom F = A$

Metamath Proof Explorer

Theorem frrlem14

Proof