tfrlem9a

Description: Lemma for transfinite recursion. Without using ax-rep , show that all the restrictions of recs are sets. (Contributed by Mario Carneiro, 16-Nov-2014)

		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	tfrlem9a	$⊢ B \in dom recs (F) \to {recs (F) ↾}_{B} \in V$

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	1	tfrlem7	$⊢ Fun recs (F)$
3		funfvop	$⊢ (Fun recs (F) \land B \in dom recs (F)) \to ⟨B, recs (F) (B)⟩ \in recs (F)$
4	2 3	mpan	$⊢ B \in dom recs (F) \to ⟨B, recs (F) (B)⟩ \in recs (F)$
5	1	recsfval	$⊢ recs (F) = ⋃ A$
6	5	eleq2i	$⊢ ⟨B, recs (F) (B)⟩ \in recs (F) \leftrightarrow ⟨B, recs (F) (B)⟩ \in ⋃ A$
7		eluni	$⊢ ⟨B, recs (F) (B)⟩ \in ⋃ A \leftrightarrow \exists g (⟨B, recs (F) (B)⟩ \in g \land g \in A)$
8	6 7	bitri	$⊢ ⟨B, recs (F) (B)⟩ \in recs (F) \leftrightarrow \exists g (⟨B, recs (F) (B)⟩ \in g \land g \in A)$
9	4 8	sylib	$⊢ B \in dom recs (F) \to \exists g (⟨B, recs (F) (B)⟩ \in g \land g \in A)$
10		simprr	$⊢ (B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \to g \in A$
11		vex	$⊢ g \in V$
12	1 11	tfrlem3a	$⊢ g \in A \leftrightarrow \exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a}))$
13	10 12	sylib	$⊢ (B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \to \exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a}))$
14	2	a1i	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to Fun recs (F)$
15		simplrr	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to g \in A$
16		elssuni	$⊢ g \in A \to g \subseteq ⋃ A$
17	15 16	syl	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to g \subseteq ⋃ A$
18	17 5	sseqtrrdi	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to g \subseteq recs (F)$
19		fndm	$⊢ g Fn z \to dom g = z$
20	19	ad2antll	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to dom g = z$
21		simprl	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to z \in On$
22	20 21	eqeltrd	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to dom g \in On$
23		eloni	$⊢ dom g \in On \to Ord dom g$
24	22 23	syl	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to Ord dom g$
25		simpll	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to B \in dom recs (F)$
26		fvexd	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to recs (F) (B) \in V$
27		simplrl	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to ⟨B, recs (F) (B)⟩ \in g$
28		df-br	$⊢ B g recs (F) (B) \leftrightarrow ⟨B, recs (F) (B)⟩ \in g$
29	27 28	sylibr	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to B g recs (F) (B)$
30		breldmg	$⊢ (B \in dom recs (F) \land recs (F) (B) \in V \land B g recs (F) (B)) \to B \in dom g$
31	25 26 29 30	syl3anc	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to B \in dom g$
32		ordelss	$⊢ (Ord dom g \land B \in dom g) \to B \subseteq dom g$
33	24 31 32	syl2anc	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to B \subseteq dom g$
34		fun2ssres	$⊢ (Fun recs (F) \land g \subseteq recs (F) \land B \subseteq dom g) \to {recs (F) ↾}_{B} = {g ↾}_{B}$
35	14 18 33 34	syl3anc	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to {recs (F) ↾}_{B} = {g ↾}_{B}$
36	11	resex	$⊢ {g ↾}_{B} \in V$
37	36	a1i	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to {g ↾}_{B} \in V$
38	35 37	eqeltrd	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land (z \in On \land g Fn z)) \to {recs (F) ↾}_{B} \in V$
39	38	expr	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land z \in On) \to (g Fn z \to {recs (F) ↾}_{B} \in V)$
40	39	adantrd	$⊢ ((B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \land z \in On) \to ((g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \to {recs (F) ↾}_{B} \in V)$
41	40	rexlimdva	$⊢ (B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \to (\exists z \in On (g Fn z \land \forall a \in z g (a) = F ({g ↾}_{a})) \to {recs (F) ↾}_{B} \in V)$
42	13 41	mpd	$⊢ (B \in dom recs (F) \land (⟨B, recs (F) (B)⟩ \in g \land g \in A)) \to {recs (F) ↾}_{B} \in V$
43	9 42	exlimddv	$⊢ B \in dom recs (F) \to {recs (F) ↾}_{B} \in V$

Metamath Proof Explorer

Theorem tfrlem9a

Proof