wfrlem14OLD

Description: Lemma for well-ordered recursion. Compute the value of C . Obsolete as of 18-Nov-2024. (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	wfrlem14OLD	$⊢ z \in (A ∖ dom F) \to (y \in (dom F \cup \{z\}) \to C (y) = G ({C ↾}_{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		elun	$⊢ y \in (dom F \cup \{z\}) \leftrightarrow (y \in dom F \lor y \in \{z\})$
7		velsn	$⊢ y \in \{z\} \leftrightarrow y = z$
8	7	orbi2i	$⊢ (y \in dom F \lor y \in \{z\}) \leftrightarrow (y \in dom F \lor y = z)$
9	6 8	bitri	$⊢ y \in (dom F \cup \{z\}) \leftrightarrow (y \in dom F \lor y = z)$
10	1 2 3	wfrlem12OLD	$⊢ y \in dom F \to F (y) = G ({F ↾}_{Pred (R, A, y)})$
11		fnfun	$⊢ C Fn (dom F \cup \{z\}) \to Fun C$
12		ssun1	$⊢ F \subseteq F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
13	12 4	sseqtrri	$⊢ F \subseteq C$
14		funssfv	$⊢ (Fun C \land F \subseteq C \land y \in dom F) \to C (y) = F (y)$
15	3	wfrdmclOLD	$⊢ y \in dom F \to Pred (R, A, y) \subseteq dom F$
16		fun2ssres	$⊢ (Fun C \land F \subseteq C \land Pred (R, A, y) \subseteq dom F) \to {C ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, y)}$
17	15 16	syl3an3	$⊢ (Fun C \land F \subseteq C \land y \in dom F) \to {C ↾}_{Pred (R, A, y)} = {F ↾}_{Pred (R, A, y)}$
18	17	fveq2d	$⊢ (Fun C \land F \subseteq C \land y \in dom F) \to G ({C ↾}_{Pred (R, A, y)}) = G ({F ↾}_{Pred (R, A, y)})$
19	14 18	eqeq12d	$⊢ (Fun C \land F \subseteq C \land y \in dom F) \to (C (y) = G ({C ↾}_{Pred (R, A, y)}) \leftrightarrow F (y) = G ({F ↾}_{Pred (R, A, y)}))$
20	13 19	mp3an2	$⊢ (Fun C \land y \in dom F) \to (C (y) = G ({C ↾}_{Pred (R, A, y)}) \leftrightarrow F (y) = G ({F ↾}_{Pred (R, A, y)}))$
21	11 20	sylan	$⊢ (C Fn (dom F \cup \{z\}) \land y \in dom F) \to (C (y) = G ({C ↾}_{Pred (R, A, y)}) \leftrightarrow F (y) = G ({F ↾}_{Pred (R, A, y)}))$
22	10 21	syl5ibr	$⊢ (C Fn (dom F \cup \{z\}) \land y \in dom F) \to (y \in dom F \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
23	22	ex	$⊢ C Fn (dom F \cup \{z\}) \to (y \in dom F \to (y \in dom F \to C (y) = G ({C ↾}_{Pred (R, A, y)})))$
24	23	pm2.43d	$⊢ C Fn (dom F \cup \{z\}) \to (y \in dom F \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
25		vsnid	$⊢ z \in \{z\}$
26		elun2	$⊢ z \in \{z\} \to z \in (dom F \cup \{z\})$
27	25 26	ax-mp	$⊢ z \in (dom F \cup \{z\})$
28	4	reseq1i	$⊢ {C ↾}_{Pred (R, A, z)} = {(F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) ↾}_{Pred (R, A, z)}$
29		resundir	$⊢ {(F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}) ↾}_{Pred (R, A, z)} = ({F ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)})$
30		wefr	$⊢ R We A \to R Fr A$
31	1 30	ax-mp	$⊢ R Fr A$
32		predfrirr	$⊢ R Fr A \to \neg z \in Pred (R, A, z)$
33		ressnop0	$⊢ \neg z \in Pred (R, A, z) \to {\{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
34	31 32 33	mp2b	$⊢ {\{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)} = \emptyset$
35	34	uneq2i	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)}) = ({F ↾}_{Pred (R, A, z)}) \cup \emptyset$
36		un0	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup \emptyset = {F ↾}_{Pred (R, A, z)}$
37	35 36	eqtri	$⊢ ({F ↾}_{Pred (R, A, z)}) \cup ({\{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} ↾}_{Pred (R, A, z)}) = {F ↾}_{Pred (R, A, z)}$
38	28 29 37	3eqtri	$⊢ {C ↾}_{Pred (R, A, z)} = {F ↾}_{Pred (R, A, z)}$
39	38	fveq2i	$⊢ G ({C ↾}_{Pred (R, A, z)}) = G ({F ↾}_{Pred (R, A, z)})$
40	39	opeq2i	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ = ⟨z, G ({F ↾}_{Pred (R, A, z)})⟩$
41		opex	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in V$
42	41	elsn	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} \leftrightarrow ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ = ⟨z, G ({F ↾}_{Pred (R, A, z)})⟩$
43	40 42	mpbir	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\}$
44		elun2	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\} \to ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
45	43 44	ax-mp	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in (F \cup \{⟨z, G ({F ↾}_{Pred (R, A, z)})⟩\})$
46	45 4	eleqtrri	$⊢ ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in C$
47		fnopfvb	$⊢ (C Fn (dom F \cup \{z\}) \land z \in (dom F \cup \{z\})) \to (C (z) = G ({C ↾}_{Pred (R, A, z)}) \leftrightarrow ⟨z, G ({C ↾}_{Pred (R, A, z)})⟩ \in C)$
48	46 47	mpbiri	$⊢ (C Fn (dom F \cup \{z\}) \land z \in (dom F \cup \{z\})) \to C (z) = G ({C ↾}_{Pred (R, A, z)})$
49	27 48	mpan2	$⊢ C Fn (dom F \cup \{z\}) \to C (z) = G ({C ↾}_{Pred (R, A, z)})$
50		fveq2	$⊢ y = z \to C (y) = C (z)$
51		predeq3	$⊢ y = z \to Pred (R, A, y) = Pred (R, A, z)$
52	51	reseq2d	$⊢ y = z \to {C ↾}_{Pred (R, A, y)} = {C ↾}_{Pred (R, A, z)}$
53	52	fveq2d	$⊢ y = z \to G ({C ↾}_{Pred (R, A, y)}) = G ({C ↾}_{Pred (R, A, z)})$
54	50 53	eqeq12d	$⊢ y = z \to (C (y) = G ({C ↾}_{Pred (R, A, y)}) \leftrightarrow C (z) = G ({C ↾}_{Pred (R, A, z)}))$
55	49 54	syl5ibrcom	$⊢ C Fn (dom F \cup \{z\}) \to (y = z \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
56	24 55	jaod	$⊢ C Fn (dom F \cup \{z\}) \to ((y \in dom F \lor y = z) \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
57	9 56	syl5bi	$⊢ C Fn (dom F \cup \{z\}) \to (y \in (dom F \cup \{z\}) \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$
58	5 57	syl	$⊢ z \in (A ∖ dom F) \to (y \in (dom F \cup \{z\}) \to C (y) = G ({C ↾}_{Pred (R, A, y)}))$

Metamath Proof Explorer

Theorem wfrlem14OLD

Proof