wfrlem15OLD

Description: Obsolete version as of 18-Nov-2024. Lemma for well-ordered recursion. When z is R minimal, C is an acceptable function. This step is where the Axiom of Replacement becomes required. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 21-Apr-2011)

	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	wfrlem15OLD	$⊢ (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)}))\}$

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 4	wfrlem13OLD	$⊢ z \in (A ∖ dom F) \to C Fn (dom F \cup \{z\})$
6	5	adantr	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to C Fn (dom F \cup \{z\})$
7	1 3	wfrlem10OLD	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) = dom F$
8		eldifi	$⊢ z \in (A ∖ dom F) \to z \in A$
9		setlikespec	$⊢ (z \in A \land R Se A) \to Pred (R, A, z) \in V$
10	8 2 9	sylancl	$⊢ z \in (A ∖ dom F) \to Pred (R, A, z) \in V$
11	10	adantr	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) \in V$
12	7 11	eqeltrrd	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to dom F \in V$
13		snex	$⊢ \{z\} \in V$
14		unexg	$⊢ (dom F \in V \land \{z\} \in V) \to dom F \cup \{z\} \in V$
15	13 14	mpan2	$⊢ dom F \in V \to dom F \cup \{z\} \in V$
16		fnex	$⊢ (C Fn (dom F \cup \{z\}) \land dom F \cup \{z\} \in V) \to C \in V$
17	15 16	sylan2	$⊢ (C Fn (dom F \cup \{z\}) \land dom F \in V) \to C \in V$
18	6 12 17	syl2anc	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to C \in V$
19	12 13 14	sylancl	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to dom F \cup \{z\} \in V$
20	3	wfrdmssOLD	$⊢ dom F \subseteq A$
21	8	snssd	$⊢ z \in (A ∖ dom F) \to \{z\} \subseteq A$
22		unss	$⊢ (dom F \subseteq A \land \{z\} \subseteq A) \leftrightarrow dom F \cup \{z\} \subseteq A$
23	22	biimpi	$⊢ (dom F \subseteq A \land \{z\} \subseteq A) \to dom F \cup \{z\} \subseteq A$
24	20 21 23	sylancr	$⊢ z \in (A ∖ dom F) \to dom F \cup \{z\} \subseteq A$
25	24	adantr	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to dom F \cup \{z\} \subseteq A$
26		elun	$⊢ y \in (dom F \cup \{z\}) \leftrightarrow (y \in dom F \lor y \in \{z\})$
27		velsn	$⊢ y \in \{z\} \leftrightarrow y = z$
28	27	orbi2i	$⊢ (y \in dom F \lor y \in \{z\}) \leftrightarrow (y \in dom F \lor y = z)$
29	26 28	bitri	$⊢ y \in (dom F \cup \{z\}) \leftrightarrow (y \in dom F \lor y = z)$
30	3	wfrdmclOLD	$⊢ y \in dom F \to Pred (R, A, y) \subseteq dom F$
31		ssun3	$⊢ Pred (R, A, y) \subseteq dom F \to Pred (R, A, y) \subseteq dom F \cup \{z\}$
32	30 31	syl	$⊢ y \in dom F \to Pred (R, A, y) \subseteq dom F \cup \{z\}$
33	32	a1i	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (y \in dom F \to Pred (R, A, y) \subseteq dom F \cup \{z\})$
34		ssun1	$⊢ dom F \subseteq dom F \cup \{z\}$
35	7 34	eqsstrdi	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to Pred (R, A, z) \subseteq dom F \cup \{z\}$
36		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
37	36	sseq1d	$⊢ y = z \to (Pred (R, A, y) \subseteq dom F \cup \{z\} \leftrightarrow Pred (R, A, z) \subseteq dom F \cup \{z\})$
38	35 37	syl5ibrcom	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (y = z \to Pred (R, A, y) \subseteq dom F \cup \{z\})$
39	33 38	jaod	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to ((y \in dom F \lor y = z) \to Pred (R, A, y) \subseteq dom F \cup \{z\})$
40	29 39	biimtrid	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (y \in (dom F \cup \{z\}) \to Pred (R, A, y) \subseteq dom F \cup \{z\})$
41	40	ralrimiv	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\}$
42	25 41	jca	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (dom F \cup \{z\} \subseteq A \land \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\})$
43	1 2 3 4	wfrlem14OLD	$⊢ z \in (A ∖ dom F) \to (y \in (dom F \cup \{z\}) \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
44	43	ralrimiv	$⊢ z \in (A ∖ dom F) \to \forall y \in (dom F \cup \{z\}) C (y) = G ({C ↾}_{Pred (R, A, y)})$
45	44	adantr	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to \forall y \in (dom F \cup \{z\}) C (y) = G ({C ↾}_{Pred (R, A, y)})$
46	6 42 45	3jca	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to (C Fn (dom F \cup \{z\}) \land (dom F \cup \{z\} \subseteq A \land \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\}) \land \forall y \in (dom F \cup \{z\}) C (y) = G ({C ↾}_{Pred (R, A, y)}))$
47		fneq2	$⊢ x = dom F \cup \{z\} \to (C Fn x \leftrightarrow C Fn (dom F \cup \{z\}))$
48		sseq1	$⊢ x = dom F \cup \{z\} \to (x \subseteq A \leftrightarrow dom F \cup \{z\} \subseteq A)$
49		sseq2	$⊢ x = dom F \cup \{z\} \to (Pred (R, A, y) \subseteq x \leftrightarrow Pred (R, A, y) \subseteq dom F \cup \{z\})$
50	49	raleqbi1dv	$⊢ x = dom F \cup \{z\} \to (\forall y \in x Pred (R, A, y) \subseteq x \leftrightarrow \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\})$
51	48 50	anbi12d	$⊢ x = dom F \cup \{z\} \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \leftrightarrow (dom F \cup \{z\} \subseteq A \land \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\}))$
52		raleq	$⊢ x = dom F \cup \{z\} \to (\forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in (dom F \cup \{z\}) C (y) = G ({C ↾}_{Pred (R, A, y)}))$
53	47 51 52	3anbi123d	$⊢ x = dom F \cup \{z\} \to ((C Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)})) \leftrightarrow (C Fn (dom F \cup \{z\}) \land (dom F \cup \{z\} \subseteq A \land \forall y \in (dom F \cup \{z\}) Pred (R, A, y) \subseteq dom F \cup \{z\}) \land \forall y \in (dom F \cup \{z\}) C (y) = G ({C ↾}_{Pred (R, A, y)})))$
54	19 46 53	spcedv	$⊢ (z \in (A ∖ dom F) \land Pred (R, (A ∖ dom F), z) = \emptyset) \to \exists x (C Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)}))$
55		fneq1	$⊢ f = C \to (f Fn x \leftrightarrow C Fn x)$
56		fveq1	$⊢ f = C \to f (y) = C (y)$
57		reseq1	$⊢ f = C \to {f ↾}_{Pred (R, A, y)} = {C ↾}_{Pred (R, A, y)}$
58	57	fveq2d	$⊢ f = C \to G ({f ↾}_{Pred (R, A, y)}) = G ({C ↾}_{Pred (R, A, y)})$
59	56 58	eqeq12d	$⊢ f = C \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \leftrightarrow C (y) = G ({C ↾}_{Pred (R, A, y)}))$
60	59	ralbidv	$⊢ f = C \to (\forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \leftrightarrow \forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)}))$
61	55 60	3anbi13d	$⊢ f = C \to ((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)})) \leftrightarrow (C Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)})))$
62	61	exbidv	$⊢ f = C \to (\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)})) \leftrightarrow \exists x (C Fn x \land (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \land \forall y \in x C (y) = G ({C ↾}_{Pred (R, A, y)})))$
63	18 54 62	elabd	$⊢ (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)}))\}$

Metamath Proof Explorer

Theorem wfrlem15OLD

Proof