tfrlem8

Description: Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994) (Proof shortened by Alan Sare, 11-Mar-2008)

		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	tfrlem8	$⊢ Ord dom recs (F)$

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	tfrlem3	$⊢ A = \{g \| \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))\}$
3	2	eqabri	$⊢ g \in A \leftrightarrow \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w}))$
4		fndm	$⊢ g Fn z \to dom g = z$
5	4	adantr	$⊢ (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to dom g = z$
6	5	eleq1d	$⊢ (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to (dom g \in On \leftrightarrow z \in On)$
7	6	biimprcd	$⊢ z \in On \to ((g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to dom g \in On)$
8	7	rexlimiv	$⊢ \exists z \in On (g Fn z \land \forall w \in z g (w) = F ({g ↾}_{w})) \to dom g \in On$
9	3 8	sylbi	$⊢ g \in A \to dom g \in On$
10		eleq1a	$⊢ dom g \in On \to (z = dom g \to z \in On)$
11	9 10	syl	$⊢ g \in A \to (z = dom g \to z \in On)$
12	11	rexlimiv	$⊢ \exists g \in A z = dom g \to z \in On$
13	12	abssi	$⊢ \{z \| \exists g \in A z = dom g\} \subseteq On$
14		ssorduni	$⊢ \{z \| \exists g \in A z = dom g\} \subseteq On \to Ord ⋃ \{z \| \exists g \in A z = dom g\}$
15	13 14	ax-mp	$⊢ Ord ⋃ \{z \| \exists g \in A z = dom g\}$
16	1	recsfval	$⊢ recs (F) = ⋃ A$
17	16	dmeqi	$⊢ dom recs (F) = dom ⋃ A$
18		dmuni	$⊢ dom ⋃ A = ⋃_{g \in A} dom g$
19		vex	$⊢ g \in V$
20	19	dmex	$⊢ dom g \in V$
21	20	dfiun2	$⊢ ⋃_{g \in A} dom g = ⋃ \{z \| \exists g \in A z = dom g\}$
22	17 18 21	3eqtri	$⊢ dom recs (F) = ⋃ \{z \| \exists g \in A z = dom g\}$
23		ordeq	$⊢ dom recs (F) = ⋃ \{z \| \exists g \in A z = dom g\} \to (Ord dom recs (F) \leftrightarrow Ord ⋃ \{z \| \exists g \in A z = dom g\})$
24	22 23	ax-mp	$⊢ Ord dom recs (F) \leftrightarrow Ord ⋃ \{z \| \exists g \in A z = dom g\}$
25	15 24	mpbir	$⊢ Ord dom recs (F)$

Metamath Proof Explorer

Theorem tfrlem8

Proof