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) (Proof revised by Scott Fenton, 18-Nov-2024.)

		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) = frecs (E, On, F \circ 2^{nd})$
3		df-frecs	$⊢ frecs (E, On, F \circ 2^{nd}) = ⋃ \{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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}))\}$
4		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) = y (F \circ 2^{nd}) ({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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)})))$
5		vex	$⊢ x \in V$
6	5	elon	$⊢ x \in On \leftrightarrow Ord x$
7		ordsson	$⊢ Ord x \to x \subseteq On$
8		ordtr	$⊢ Ord x \to Tr x$
9	7 8	jca	$⊢ Ord x \to (x \subseteq On \land Tr x)$
10		epweon	$⊢ E We On$
11		wess	$⊢ x \subseteq On \to (E We On \to E We x)$
12	10 11	mpi	$⊢ x \subseteq On \to E We x$
13	12	anim1ci	$⊢ (x \subseteq On \land Tr x) \to (Tr x \land E We x)$
14		df-ord	$⊢ Ord x \leftrightarrow (Tr x \land E We x)$
15	13 14	sylibr	$⊢ (x \subseteq On \land Tr x) \to Ord x$
16	9 15	impbii	$⊢ Ord x \leftrightarrow (x \subseteq On \land Tr x)$
17		dftr3	$⊢ Tr x \leftrightarrow \forall y \in x y \subseteq x$
18		ssel2	$⊢ (x \subseteq On \land y \in x) \to y \in On$
19		predon	$⊢ y \in On \to Pred (E, On, y) = y$
20	19	sseq1d	$⊢ y \in On \to (Pred (E, On, y) \subseteq x \leftrightarrow y \subseteq x)$
21	18 20	syl	$⊢ (x \subseteq On \land y \in x) \to (Pred (E, On, y) \subseteq x \leftrightarrow y \subseteq x)$
22	21	ralbidva	$⊢ x \subseteq On \to (\forall y \in x Pred (E, On, y) \subseteq x \leftrightarrow \forall y \in x y \subseteq x)$
23	17 22	bitr4id	$⊢ x \subseteq On \to (Tr x \leftrightarrow \forall y \in x Pred (E, On, y) \subseteq x)$
24	23	pm5.32i	$⊢ (x \subseteq On \land Tr x) \leftrightarrow (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x)$
25	6 16 24	3bitri	$⊢ x \in On \leftrightarrow (x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x)$
26	25	anbi1i	$⊢ (x \in On \land \forall y \in x f (y) = y (F \circ 2^{nd}) ({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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}))$
27		onelon	$⊢ (x \in On \land y \in x) \to y \in On$
28	27 19	syl	$⊢ (x \in On \land y \in x) \to Pred (E, On, y) = y$
29	28	reseq2d	$⊢ (x \in On \land y \in x) \to {f ↾}_{Pred (E, On, y)} = {f ↾}_{y}$
30	29	oveq2d	$⊢ (x \in On \land y \in x) \to y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}) = y (F \circ 2^{nd}) ({f ↾}_{y})$
31		id	$⊢ y \in x \to y \in x$
32		vex	$⊢ f \in V$
33	32	resex	$⊢ {f ↾}_{y} \in V$
34	33	a1i	$⊢ y \in x \to {f ↾}_{y} \in V$
35	31 34	opco2	$⊢ y \in x \to y (F \circ 2^{nd}) ({f ↾}_{y}) = F ({f ↾}_{y})$
36	35	adantl	$⊢ (x \in On \land y \in x) \to y (F \circ 2^{nd}) ({f ↾}_{y}) = F ({f ↾}_{y})$
37	30 36	eqtrd	$⊢ (x \in On \land y \in x) \to y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}) = F ({f ↾}_{y})$
38	37	eqeq2d	$⊢ (x \in On \land y \in x) \to (f (y) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}) \leftrightarrow f (y) = F ({f ↾}_{y}))$
39	38	ralbidva	$⊢ x \in On \to (\forall y \in x f (y) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}) \leftrightarrow \forall y \in x f (y) = F ({f ↾}_{y}))$
40	39	pm5.32i	$⊢ (x \in On \land \forall y \in x f (y) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))$
41	26 40	bitr3i	$⊢ ((x \subseteq On \land \forall y \in x Pred (E, On, y) \subseteq x) \land \forall y \in x f (y) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y}))$
42	41	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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}))) \leftrightarrow (f Fn x \land (x \in On \land \forall y \in x f (y) = F ({f ↾}_{y})))$
43		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})))$
44	4 42 43	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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)})) \leftrightarrow (x \in On \land (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y})))$
45	44	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) = y (F \circ 2^{nd}) ({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})))$
46		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})))$
47	45 46	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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)})) \leftrightarrow \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))$
48	47	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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}))\} = \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
49	48	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) = y (F \circ 2^{nd}) ({f ↾}_{Pred (E, On, y)}))\} = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
50	3 49	eqtri	$⊢ frecs (E, On, F \circ 2^{nd}) = ⋃ \{f \| \exists x \in On (f Fn x \land \forall y \in x f (y) = F ({f ↾}_{y}))\}$
51	1 2 50	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