dfrecs3

Description: The old definition of transfinite recursion. This version is preferred for development, as it demonstrates the properties of transfinite recursion without relying on well-ordered recursion. (Contributed by Scott Fenton, 3-Aug-2020)

		Ref	Expression
	Assertion	dfrecs3	$⊢ recs (F) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$

Proof

Step	Hyp	Ref	Expression
1		df-recs	$⊢ recs (F) = wrecs (E, On, F)$
2		df-wrecs	$⊢ wrecs (E, On, F) = ⋃ \{f \| \exists x (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}))\}$
3		3anass	$⊢ (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (f Fn x \land ((x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})))$
4		vex	$⊢ x \in V$
5	4	elon	$⊢ x \in On \leftrightarrow Ord x$
6		ordsson	$⊢ Ord x \to x \subseteq On$
7		ordtr	$⊢ Ord x \to Tr x$
8	6 7	jca	$⊢ Ord x \to (x \subseteq On \land Tr x)$
9		epweon	$⊢ E We On$
10		wess	$⊢ x \subseteq On \to (E We On \to E We x)$
11	9 10	mpi	$⊢ x \subseteq On \to E We x$
12	11	anim1ci	$⊢ (x \subseteq On \land Tr x) \to (Tr x \land E We x)$
13		df-ord	$⊢ Ord x \leftrightarrow (Tr x \land E We x)$
14	12 13	sylibr	$⊢ (x \subseteq On \land Tr x) \to Ord x$
15	8 14	impbii	$⊢ Ord x \leftrightarrow (x \subseteq On \land Tr x)$
16		dftr3	$⊢ Tr x \leftrightarrow \forall y \in x y \subseteq x$
17		ssel2	$⊢ (x \subseteq On \land y \in x) \to y \in On$
18		predon	$⊢ y \in On \to Pred (E, On, y) = y$
19	18	sseq1d	$⊢ y \in On \to (Pred (E, On, y) \subseteq x \leftrightarrow y \subseteq x)$
20	17 19	syl	$⊢ (x \subseteq On \land y \in x) \to (Pred (E, On, y) \subseteq x \leftrightarrow y \subseteq x)$
21	20	ralbidva	$⊢ x \subseteq On \to (\forall y \in x Pred (E, On, y) \subseteq x \leftrightarrow \forall y \in x y \subseteq x)$
22	16 21	bitr4id	$⊢ x \subseteq On \to (Tr x \leftrightarrow \forall y \in x Pred (E, On, y) \subseteq x)$
23	22	pm5.32i	$⊢ (x \subseteq On \land Tr x) \leftrightarrow (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x)$
24	5 15 23	3bitri	$⊢ x \in On \leftrightarrow (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x)$
25	24	anbi1i	$⊢ (x \in On \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow ((x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}))$
26		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
27	18	reseq2d	$⊢ y \in On \to {f ↾}_{Pred (E, On, y)} = {f ↾}_{y}$
28	27	fveq2d	$⊢ y \in On \to F ({f ↾}_{Pred (E, On, y)}) = F ({f ↾}_{y})$
29	28	eqeq2d	$⊢ y \in On \to (f (y) = F ({f ↾}_{Pred (E, On, y)}) \leftrightarrow f (y) = F ({f ↾}_{y}))$
30	26 29	syl	$⊢ (x \in On \land y \in x) \to (f (y) = F ({f ↾}_{Pred (E, On, y)}) \leftrightarrow f (y) = F ({f ↾}_{y}))$
31	30	ralbidva	$⊢ x \in On \to (\forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}) \leftrightarrow \forall y \in x f (y) = F ({f ↾}_{y}))$
32	31	pm5.32i	$⊢ (x \in On \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))$
33	25 32	bitr3i	$⊢ ((x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))$
34	33	anbi2i	$⊢ (f Fn x \land ((x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}))) \leftrightarrow (f Fn x \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))$
35		an12	$⊢ (f Fn x \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))) \leftrightarrow (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
36	3 34 35	3bitri	$⊢ (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
37	36	exbii	$⊢ \exists x (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow \exists x (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
38		df-rex	$⊢ \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})) \leftrightarrow \exists x (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
39	37 38	bitr4i	$⊢ \exists x (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)})) \leftrightarrow \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))$
40	39	abbii	$⊢ \{f \| \exists x (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
41	40	unieqi	$⊢ ⋃ \{f \| \exists x (f Fn x \land (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = F ({f ↾}_{Pred (E, On, y)}))\} = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
42	1 2 41	3eqtri	$⊢ recs (F) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$

Metamath Proof Explorer

Theorem dfrecs3

Proof