Theorem tz9.12lem2

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003)

	Ref	Expression
Hypotheses	tz9.12lem.1	$$⊢A\in \mathrm{V}$$
	tz9.12lem.2	$$⊢F=\left(z\in \mathrm{V}⟼\bigcap \left\{v\in \mathrm{On}|z\in R_1\left(v\right)\right\}\right)$$
Assertion	tz9.12lem2	$$⊢\mathrm{suc}\bigcup F\left[A\right]\in \mathrm{On}$$

Proof

Step	Hyp	Ref	Expression
1		tz9.12lem.1	$$⊢A\in \mathrm{V}$$
2		tz9.12lem.2	$$⊢F=\left(z\in \mathrm{V}⟼\bigcap \left\{v\in \mathrm{On}|z\in R_1\left(v\right)\right\}\right)$$
3	1 2	tz9.12lem1	$$⊢F\left[A\right]\subseteq \mathrm{On}$$
4	2	funmpt2	$$⊢\mathrm{Fun}F$$
5	1	funimaex	$$⊢\mathrm{Fun}F\to F\left[A\right]\in \mathrm{V}$$
6	4 5	ax-mp	$$⊢F\left[A\right]\in \mathrm{V}$$
7	6	ssonunii	$$⊢F\left[A\right]\subseteq \mathrm{On}\to \bigcup F\left[A\right]\in \mathrm{On}$$
8	3 7	ax-mp	$$⊢\bigcup F\left[A\right]\in \mathrm{On}$$
9	8	onsuci	$$⊢\mathrm{suc}\bigcup F\left[A\right]\in \mathrm{On}$$