frrlem13

Description: Lemma for well-founded recursion. Assuming that S is a subset of A and that z is R -minimal, then C is an acceptable function. (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$
Assertion	frrlem13	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \in B$

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		eldifi	$⊢ z \in (A ∖ dom F) \to z \in A$
11	10 8	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to S \in V$
12	11	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to S \in V$
13		inex1g	$⊢ S \in V \to S \cap dom F \in V$
14		snex	$⊢ \{z\} \in V$
15		unexg	$⊢ (S \cap dom F \in V \land \{z\} \in V) \to (S \cap dom F) \cup \{z\} \in V$
16	13 14 15	sylancl	$⊢ S \in V \to (S \cap dom F) \cup \{z\} \in V$
17	12 16	syl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (S \cap dom F) \cup \{z\} \in V$
18	1 2 3 4	frrlem11	$⊢ (φ \land z \in (A ∖ dom F)) \to C Fn ((S \cap dom F) \cup \{z\})$
19	18	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C Fn ((S \cap dom F) \cup \{z\})$
20		inss1	$⊢ S \cap dom F \subseteq S$
21	10 9	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to S \subseteq A$
22	21	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to S \subseteq A$
23	20 22	sstrid	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to S \cap dom F \subseteq A$
24	10	adantl	$⊢ (φ \land z \in (A ∖ dom F)) \to z \in A$
25	24	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to z \in A$
26	25	snssd	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to \{z\} \subseteq A$
27	23 26	unssd	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (S \cap dom F) \cup \{z\} \subseteq A$
28		elun	$⊢ w \in ((S \cap dom F) \cup \{z\}) \leftrightarrow (w \in (S \cap dom F) \lor w \in \{z\})$
29		elin	$⊢ w \in (S \cap dom F) \leftrightarrow (w \in S \land w \in dom F)$
30		velsn	$⊢ w \in \{z\} \leftrightarrow w = z$
31	29 30	orbi12i	$⊢ (w \in (S \cap dom F) \lor w \in \{z\}) \leftrightarrow ((w \in S \land w \in dom F) \lor w = z)$
32	28 31	bitri	$⊢ w \in ((S \cap dom F) \cup \{z\}) \leftrightarrow ((w \in S \land w \in dom F) \lor w = z)$
33	10 7	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to \forall w \in S Pred (R, A, w) \subseteq S$
34	33	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to \forall w \in S Pred (R, A, w) \subseteq S$
35		rsp	$⊢ \forall w \in S Pred (R, A, w) \subseteq S \to (w \in S \to Pred (R, A, w) \subseteq S)$
36	34 35	syl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (w \in S \to Pred (R, A, w) \subseteq S)$
37	1 2	frrlem8	$⊢ w \in dom F \to Pred (R, A, w) \subseteq dom F$
38	36 37	anim12d1	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to ((w \in S \land w \in dom F) \to (Pred (R, A, w) \subseteq S \land Pred (R, A, w) \subseteq dom F))$
39		ssin	$⊢ (Pred (R, A, w) \subseteq S \land Pred (R, A, w) \subseteq dom F) \leftrightarrow Pred (R, A, w) \subseteq S \cap dom F$
40	38 39	syl6ib	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to ((w \in S \land w \in dom F) \to Pred (R, A, w) \subseteq S \cap dom F)$
41	10 6	sylan2	$⊢ (φ \land z \in (A ∖ dom F)) \to Pred (R, A, z) \subseteq S$
42	41	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to Pred (R, A, z) \subseteq S$
43		preddif	$⊢ Pred (R, (A ∖ dom F), z) = Pred (R, A, z) ∖ Pred (R, dom F, z)$
44	43	eqeq1i	$⊢ Pred (R, (A ∖ dom F), z) = \emptyset \leftrightarrow Pred (R, A, z) ∖ Pred (R, dom F, z) = \emptyset$
45		ssdif0	$⊢ Pred (R, A, z) \subseteq Pred (R, dom F, z) \leftrightarrow Pred (R, A, z) ∖ Pred (R, dom F, z) = \emptyset$
46	44 45	sylbb2	$⊢ Pred (R, (A ∖ dom F), z) = \emptyset \to Pred (R, A, z) \subseteq Pred (R, dom F, z)$
47		predss	$⊢ Pred (R, dom F, z) \subseteq dom F$
48	46 47	sstrdi	$⊢ Pred (R, (A ∖ dom F), z) = \emptyset \to Pred (R, A, z) \subseteq dom F$
49	48	adantl	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) \subseteq dom F$
50	49	adantl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to Pred (R, A, z) \subseteq dom F$
51	42 50	ssind	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to Pred (R, A, z) \subseteq S \cap dom F$
52		predeq3	$⊢ w = z \to Pred (R, A, w) = Pred (R, A, z)$
53	52	sseq1d	$⊢ w = z \to (Pred (R, A, w) \subseteq S \cap dom F \leftrightarrow Pred (R, A, z) \subseteq S \cap dom F)$
54	51 53	syl5ibrcom	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (w = z \to Pred (R, A, w) \subseteq S \cap dom F)$
55	40 54	jaod	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (((w \in S \land w \in dom F) \lor w = z) \to Pred (R, A, w) \subseteq S \cap dom F)$
56	32 55	syl5bi	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (w \in ((S \cap dom F) \cup \{z\}) \to Pred (R, A, w) \subseteq S \cap dom F)$
57	56	imp	$⊢ ((φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \land w \in ((S \cap dom F) \cup \{z\})) \to Pred (R, A, w) \subseteq S \cap dom F$
58		ssun1	$⊢ S \cap dom F \subseteq (S \cap dom F) \cup \{z\}$
59	57 58	sstrdi	$⊢ ((φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \land w \in ((S \cap dom F) \cup \{z\})) \to Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}$
60	59	ralrimiva	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}$
61	27 60	jca	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to ((S \cap dom F) \cup \{z\} \subseteq A \land \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\})$
62	1 2 3 4 5 6 7	frrlem12	$⊢ (φ \land z \in (A ∖ dom F) \land w \in ((S \cap dom F) \cup \{z\})) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$
63	62	3expa	$⊢ ((φ \land z \in (A ∖ dom F)) \land w \in ((S \cap dom F) \cup \{z\})) \to C (w) = w G ({C ↾}_{Pred (R, A, w)})$
64	63	ralrimiva	$⊢ (φ \land z \in (A ∖ dom F)) \to \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)})$
65	64	adantrr	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)})$
66		fneq2	$⊢ t = (S \cap dom F) \cup \{z\} \to (C Fn t \leftrightarrow C Fn ((S \cap dom F) \cup \{z\}))$
67		sseq1	$⊢ t = (S \cap dom F) \cup \{z\} \to (t \subseteq A \leftrightarrow (S \cap dom F) \cup \{z\} \subseteq A)$
68		sseq2	$⊢ t = (S \cap dom F) \cup \{z\} \to (Pred (R, A, w) \subseteq t \leftrightarrow Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\})$
69	68	raleqbi1dv	$⊢ t = (S \cap dom F) \cup \{z\} \to (\forall w \in t Pred (R, A, w) \subseteq t \leftrightarrow \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\})$
70	67 69	anbi12d	$⊢ t = (S \cap dom F) \cup \{z\} \to ((t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \leftrightarrow ((S \cap dom F) \cup \{z\} \subseteq A \land \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}))$
71		raleq	$⊢ t = (S \cap dom F) \cup \{z\} \to (\forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)}) \leftrightarrow \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
72	66 70 71	3anbi123d	$⊢ t = (S \cap dom F) \cup \{z\} \to ((C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})) \leftrightarrow (C Fn ((S \cap dom F) \cup \{z\}) \land ((S \cap dom F) \cup \{z\} \subseteq A \land \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}) \land \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
73	72	spcegv	$⊢ (S \cap dom F) \cup \{z\} \in V \to ((C Fn ((S \cap dom F) \cup \{z\}) \land ((S \cap dom F) \cup \{z\} \subseteq A \land \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}) \land \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)})) \to \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
74	73	imp	$⊢ ((S \cap dom F) \cup \{z\} \in V \land (C Fn ((S \cap dom F) \cup \{z\}) \land ((S \cap dom F) \cup \{z\} \subseteq A \land \forall w \in ((S \cap dom F) \cup \{z\}) Pred (R, A, w) \subseteq (S \cap dom F) \cup \{z\}) \land \forall w \in ((S \cap dom F) \cup \{z\}) C (w) = w G ({C ↾}_{Pred (R, A, w)}))) \to \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
75	17 19 61 65 74	syl13anc	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
76	1 2 3	frrlem9	$⊢ φ \to Fun F$
77		resfunexg	$⊢ (Fun F \land S \in V) \to {F ↾}_{S} \in V$
78	76 12 77	syl2an2r	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to {F ↾}_{S} \in V$
79		snex	$⊢ \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} \in V$
80		unexg	$⊢ ({F ↾}_{S} \in V \land \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} \in V) \to ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} \in V$
81	78 79 80	sylancl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to ({F ↾}_{S}) \cup \{⟨z, z G ({F ↾}_{Pred (R, A, z)})⟩\} \in V$
82	4 81	eqeltrid	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \in V$
83		fneq1	$⊢ c = C \to (c Fn t \leftrightarrow C Fn t)$
84		fveq1	$⊢ c = C \to c (w) = C (w)$
85		reseq1	$⊢ c = C \to {c ↾}_{Pred (R, A, w)} = {C ↾}_{Pred (R, A, w)}$
86	85	oveq2d	$⊢ c = C \to w G ({c ↾}_{Pred (R, A, w)}) = w G ({C ↾}_{Pred (R, A, w)})$
87	84 86	eqeq12d	$⊢ c = C \to (c (w) = w G ({c ↾}_{Pred (R, A, w)}) \leftrightarrow C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
88	87	ralbidv	$⊢ c = C \to (\forall w \in t c (w) = w G ({c ↾}_{Pred (R, A, w)}) \leftrightarrow \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)}))$
89	83 88	3anbi13d	$⊢ c = C \to ((c Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t c (w) = w G ({c ↾}_{Pred (R, A, w)})) \leftrightarrow (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
90	89	exbidv	$⊢ c = C \to (\exists t (c Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t c (w) = w G ({c ↾}_{Pred (R, A, w)})) \leftrightarrow \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
91	1	frrlem1	$⊢ B = \{c \| \exists t (c Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t c (w) = w G ({c ↾}_{Pred (R, A, w)}))\}$
92	90 91	elab2g	$⊢ C \in V \to (C \in B \leftrightarrow \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
93	82 92	syl	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to (C \in B \leftrightarrow \exists t (C Fn t \land (t \subseteq A \land \forall w \in t Pred (R, A, w) \subseteq t) \land \forall w \in t C (w) = w G ({C ↾}_{Pred (R, A, w)})))$
94	75 93	mpbird	$⊢ (φ \land (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset)) \to C \in B$

Metamath Proof Explorer

Theorem frrlem13

Proof