tfrlem9

Description: Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994)

		Ref	Expression
	Hypothesis	tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
	Assertion	tfrlem9	$⊢ B \in dom recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})$

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	$⊢ A = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
2		eldm2g	$⊢ B \in dom recs (F) \to (B \in dom recs (F) \leftrightarrow \exists z ⟨B, z⟩ \in recs (F))$
3	2	ibi	$⊢ B \in dom recs (F) \to \exists z ⟨B, z⟩ \in recs (F)$
4		dfrecs3	$⊢ recs (F) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
5	4	eleq2i	$⊢ ⟨B, z⟩ \in recs (F) \leftrightarrow ⟨B, z⟩ \in ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
6		eluniab	$⊢ ⟨B, z⟩ \in ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\} \leftrightarrow \exists f (⟨B, z⟩ \in f \land \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
7	5 6	bitri	$⊢ ⟨B, z⟩ \in recs (F) \leftrightarrow \exists f (⟨B, z⟩ \in f \land \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
8		fnop	$⊢ (f Fn x \land ⟨B, z⟩ \in f) \to B \in x$
9		rspe	$⊢ (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))$
10	1	eqabri	$⊢ f \in A \leftrightarrow \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))$
11		elssuni	$⊢ f \in A \to f \subseteq ⋃ A$
12	1	recsfval	$⊢ recs (F) = ⋃ A$
13	11 12	sseqtrrdi	$⊢ f \in A \to f \subseteq recs (F)$
14	10 13	sylbir	$⊢ \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \to f \subseteq recs (F)$
15	9 14	syl	$⊢ (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to f \subseteq recs (F)$
16		fveq2	$⊢ y = B \to f (y) = f (B)$
17		reseq2	$⊢ y = B \to {f ↾}_{y} = {f ↾}_{B}$
18	17	fveq2d	$⊢ y = B \to F ({f ↾}_{y}) = F ({f ↾}_{B})$
19	16 18	eqeq12d	$⊢ y = B \to (f (y) = F ({f ↾}_{y}) \leftrightarrow f (B) = F ({f ↾}_{B}))$
20	19	rspcv	$⊢ B \in x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to f (B) = F ({f ↾}_{B}))$
21		fndm	$⊢ f Fn x \to dom f = x$
22	21	eleq2d	$⊢ f Fn x \to (B \in dom f \leftrightarrow B \in x)$
23	1	tfrlem7	$⊢ Fun recs (F)$
24		funssfv	$⊢ (Fun recs (F) \land f \subseteq recs (F) \land B \in dom f) \to recs (F) (B) = f (B)$
25	23 24	mp3an1	$⊢ (f \subseteq recs (F) \land B \in dom f) \to recs (F) (B) = f (B)$
26	25	adantrl	$⊢ (f \subseteq recs (F) \land ((f Fn x \land x \in On) \land B \in dom f)) \to recs (F) (B) = f (B)$
27	21	eleq1d	$⊢ f Fn x \to (dom f \in On \leftrightarrow x \in On)$
28		onelss	$⊢ dom f \in On \to (B \in dom f \to B \subseteq dom f)$
29	27 28	biimtrrdi	$⊢ f Fn x \to (x \in On \to (B \in dom f \to B \subseteq dom f))$
30	29	imp31	$⊢ ((f Fn x \land x \in On) \land B \in dom f) \to B \subseteq dom f$
31		fun2ssres	$⊢ (Fun recs (F) \land f \subseteq recs (F) \land B \subseteq dom f) \to {recs (F) ↾}_{B} = {f ↾}_{B}$
32	31	fveq2d	$⊢ (Fun recs (F) \land f \subseteq recs (F) \land B \subseteq dom f) \to F ({recs (F) ↾}_{B}) = F ({f ↾}_{B})$
33	23 32	mp3an1	$⊢ (f \subseteq recs (F) \land B \subseteq dom f) \to F ({recs (F) ↾}_{B}) = F ({f ↾}_{B})$
34	30 33	sylan2	$⊢ (f \subseteq recs (F) \land ((f Fn x \land x \in On) \land B \in dom f)) \to F ({recs (F) ↾}_{B}) = F ({f ↾}_{B})$
35	26 34	eqeq12d	$⊢ (f \subseteq recs (F) \land ((f Fn x \land x \in On) \land B \in dom f)) \to (recs (F) (B) = F ({recs (F) ↾}_{B}) \leftrightarrow f (B) = F ({f ↾}_{B}))$
36	35	exbiri	$⊢ f \subseteq recs (F) \to (((f Fn x \land x \in On) \land B \in dom f) \to (f (B) = F ({f ↾}_{B}) \to recs (F) (B) = F ({recs (F) ↾}_{B})))$
37	36	com3l	$⊢ ((f Fn x \land x \in On) \land B \in dom f) \to (f (B) = F ({f ↾}_{B}) \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))$
38	37	exp31	$⊢ f Fn x \to (x \in On \to (B \in dom f \to (f (B) = F ({f ↾}_{B}) \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
39	38	com34	$⊢ f Fn x \to (x \in On \to (f (B) = F ({f ↾}_{B}) \to (B \in dom f \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
40	39	com24	$⊢ f Fn x \to (B \in dom f \to (f (B) = F ({f ↾}_{B}) \to (x \in On \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
41	22 40	sylbird	$⊢ f Fn x \to (B \in x \to (f (B) = F ({f ↾}_{B}) \to (x \in On \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
42	41	com3l	$⊢ B \in x \to (f (B) = F ({f ↾}_{B}) \to (f Fn x \to (x \in On \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
43	20 42	syld	$⊢ B \in x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to (f Fn x \to (x \in On \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
44	43	com24	$⊢ B \in x \to (x \in On \to (f Fn x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
45	44	imp4d	$⊢ B \in x \to ((x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to (f \subseteq recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})))$
46	15 45	mpdi	$⊢ B \in x \to ((x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to recs (F) (B) = F ({recs (F) ↾}_{B}))$
47	8 46	syl	$⊢ (f Fn x \land ⟨B, z⟩ \in f) \to ((x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to recs (F) (B) = F ({recs (F) ↾}_{B}))$
48	47	exp4d	$⊢ (f Fn x \land ⟨B, z⟩ \in f) \to (x \in On \to (f Fn x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to recs (F) (B) = F ({recs (F) ↾}_{B}))))$
49	48	ex	$⊢ f Fn x \to (⟨B, z⟩ \in f \to (x \in On \to (f Fn x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
50	49	com4r	$⊢ f Fn x \to (f Fn x \to (⟨B, z⟩ \in f \to (x \in On \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to recs (F) (B) = F ({recs (F) ↾}_{B})))))$
51	50	pm2.43i	$⊢ f Fn x \to (⟨B, z⟩ \in f \to (x \in On \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to recs (F) (B) = F ({recs (F) ↾}_{B}))))$
52	51	com3l	$⊢ ⟨B, z⟩ \in f \to (x \in On \to (f Fn x \to (\forall y \in x f (y) = F ({f ↾}_{y}) \to recs (F) (B) = F ({recs (F) ↾}_{B}))))$
53	52	imp4a	$⊢ ⟨B, z⟩ \in f \to (x \in On \to ((f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \to recs (F) (B) = F ({recs (F) ↾}_{B})))$
54	53	rexlimdv	$⊢ ⟨B, z⟩ \in f \to (\exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \to recs (F) (B) = F ({recs (F) ↾}_{B}))$
55	54	imp	$⊢ (⟨B, z⟩ \in f \land \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to recs (F) (B) = F ({recs (F) ↾}_{B})$
56	55	exlimiv	$⊢ \exists f (⟨B, z⟩ \in f \land \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))) \to recs (F) (B) = F ({recs (F) ↾}_{B})$
57	7 56	sylbi	$⊢ ⟨B, z⟩ \in recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})$
58	57	exlimiv	$⊢ \exists z ⟨B, z⟩ \in recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})$
59	3 58	syl	$⊢ B \in dom recs (F) \to recs (F) (B) = F ({recs (F) ↾}_{B})$

Metamath Proof Explorer

Theorem tfrlem9

Proof