wfrlem12

Description: Lemma for well-ordered recursion. Here, we compute the value of the recursive definition generator. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	wfrfun.1	$⊢ R We A$
	wfrfun.2	$⊢ R Se A$
	wfrfun.3	$⊢ F = wrecs (R, A, G)$
Assertion	wfrlem12	$⊢ y \in dom F \to F (y) = G ({F ↾}_{Pred (R, A, y)})$

Proof

Step	Hyp	Ref	Expression
1		wfrfun.1	$⊢ R We A$
2		wfrfun.2	$⊢ R Se A$
3		wfrfun.3	$⊢ F = wrecs (R, A, G)$
4		vex	$⊢ y \in V$
5	4	eldm2	$⊢ y \in dom F \leftrightarrow \exists z ⟨y, z⟩ \in F$
6		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)}))\}$
7	3 6	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)}))\}$
8	7	eleq2i	$⊢ ⟨y, z⟩ \in F \leftrightarrow ⟨y, z⟩ \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)}))\}$
9		eluniab	$⊢ ⟨y, z⟩ \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)}))\} \leftrightarrow \exists f (⟨y, z⟩ \in f \land \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)})))$
10	8 9	bitri	$⊢ ⟨y, z⟩ \in F \leftrightarrow \exists f (⟨y, z⟩ \in f \land \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)})))$
11		abid	$⊢ f \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)}))\} \leftrightarrow \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)}))$
12		elssuni	$⊢ f \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 f \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)}))\}$
13	12 7	sseqtrrdi	$⊢ f \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 f \subseteq F$
14	11 13	sylbir	$⊢ \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 f \subseteq F$
15		fnop	$⊢ (f Fn x \land ⟨y, z⟩ \in f) \to y \in x$
16	15	ex	$⊢ f Fn x \to (⟨y, z⟩ \in f \to y \in x)$
17		rsp	$⊢ \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (y \in x \to f (y) = G ({f ↾}_{Pred (R, A, y)}))$
18	17	impcom	$⊢ (y \in x \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)})) \to f (y) = G ({f ↾}_{Pred (R, A, y)})$
19		rsp	$⊢ \forall y \in x Pred (R, A, y) \subseteq x \to (y \in x \to Pred (R, A, y) \subseteq x)$
20		fndm	$⊢ f Fn x \to dom f = x$
21	20	sseq2d	$⊢ f Fn x \to (Pred (R, A, y) \subseteq dom f \leftrightarrow Pred (R, A, y) \subseteq x)$
22	20	eleq2d	$⊢ f Fn x \to (y \in dom f \leftrightarrow y \in x)$
23	21 22	anbi12d	$⊢ f Fn x \to ((Pred (R, A, y) \subseteq dom f \land y \in dom f) \leftrightarrow (Pred (R, A, y) \subseteq x \land y \in x))$
24	23	biimprd	$⊢ f Fn x \to ((Pred (R, A, y) \subseteq x \land y \in x) \to (Pred (R, A, y) \subseteq dom f \land y \in dom f))$
25	24	expd	$⊢ f Fn x \to (Pred (R, A, y) \subseteq x \to (y \in x \to (Pred (R, A, y) \subseteq dom f \land y \in dom f)))$
26	25	impcom	$⊢ (Pred (R, A, y) \subseteq x \land f Fn x) \to (y \in x \to (Pred (R, A, y) \subseteq dom f \land y \in dom f))$
27	1 2 3	wfrfun	$⊢ Fun F$
28		funssfv	$⊢ (Fun F \land f \subseteq F \land y \in dom f) \to F (y) = f (y)$
29	28	3adant3l	$⊢ (Fun F \land f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to F (y) = f (y)$
30		fun2ssres	$⊢ (Fun F \land f \subseteq F \land Pred (R, A, y) \subseteq dom f) \to {F ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (R, A, y)}$
31	30	3adant3r	$⊢ (Fun F \land f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to {F ↾}_{Pred (R, A, y)} = {f ↾}_{Pred (R, A, y)}$
32	31	fveq2d	$⊢ (Fun F \land f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to G ({F ↾}_{Pred (R, A, y)}) = G ({f ↾}_{Pred (R, A, y)})$
33	29 32	eqeq12d	$⊢ (Fun F \land f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to (F (y) = G ({F ↾}_{Pred (R, A, y)}) \leftrightarrow f (y) = G ({f ↾}_{Pred (R, A, y)}))$
34	33	biimprd	$⊢ (Fun F \land f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to F (y) = G ({F ↾}_{Pred (R, A, y)}))$
35	27 34	mp3an1	$⊢ (f \subseteq F \land (Pred (R, A, y) \subseteq dom f \land y \in dom f)) \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to F (y) = G ({F ↾}_{Pred (R, A, y)}))$
36	35	expcom	$⊢ (Pred (R, A, y) \subseteq dom f \land y \in dom f) \to (f \subseteq F \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to F (y) = G ({F ↾}_{Pred (R, A, y)})))$
37	36	com23	$⊢ (Pred (R, A, y) \subseteq dom f \land y \in dom f) \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))$
38	26 37	syl6com	$⊢ y \in x \to ((Pred (R, A, y) \subseteq x \land f Fn x) \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)}))))$
39	38	expd	$⊢ y \in x \to (Pred (R, A, y) \subseteq x \to (f Fn x \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
40	39	com34	$⊢ y \in x \to (Pred (R, A, y) \subseteq x \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f Fn x \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
41	19 40	sylcom	$⊢ \forall y \in x Pred (R, A, y) \subseteq x \to (y \in x \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f Fn x \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
42	41	adantl	$⊢ (x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (y \in x \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f Fn x \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
43	42	com14	$⊢ f Fn x \to (y \in x \to (f (y) = G ({f ↾}_{Pred (R, A, y)}) \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
44	18 43	syl7	$⊢ f Fn x \to (y \in x \to ((y \in x \land \forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)})) \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
45	44	exp4a	$⊢ f Fn x \to (y \in x \to (y \in x \to (\forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)}))))))$
46	45	pm2.43d	$⊢ f Fn x \to (y \in x \to (\forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
47	46	com34	$⊢ f Fn x \to (y \in x \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (\forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
48	16 47	syldc	$⊢ ⟨y, z⟩ \in f \to (f Fn x \to ((x \subseteq A \land \forall y \in x Pred (R, A, y) \subseteq x) \to (\forall y \in x f (y) = G ({f ↾}_{Pred (R, A, y)}) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))))$
49	48	3impd	$⊢ ⟨y, z⟩ \in f \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)})) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))$
50	49	exlimdv	$⊢ ⟨y, z⟩ \in f \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)})) \to (f \subseteq F \to F (y) = G ({F ↾}_{Pred (R, A, y)})))$
51	14 50	mpdi	$⊢ ⟨y, z⟩ \in f \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)})) \to F (y) = G ({F ↾}_{Pred (R, A, y)}))$
52	51	imp	$⊢ (⟨y, z⟩ \in f \land \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 F (y) = G ({F ↾}_{Pred (R, A, y)})$
53	52	exlimiv	$⊢ \exists f (⟨y, z⟩ \in f \land \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 F (y) = G ({F ↾}_{Pred (R, A, y)})$
54	10 53	sylbi	$⊢ ⟨y, z⟩ \in F \to F (y) = G ({F ↾}_{Pred (R, A, y)})$
55	54	exlimiv	$⊢ \exists z ⟨y, z⟩ \in F \to F (y) = G ({F ↾}_{Pred (R, A, y)})$
56	5 55	sylbi	$⊢ y \in dom F \to F (y) = G ({F ↾}_{Pred (R, A, y)})$

Metamath Proof Explorer

Theorem wfrlem12

Proof