Theorem r1elssi

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. One direction of r1elss that doesn't need A to be a set. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	r1elssi	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq \bigcup R_1\left[\mathrm{On}\right]$$

Proof

Step	Hyp	Ref	Expression
1		triun	$$⊢\forall x\in \mathrm{On}\mathrm{Tr}{R}_1\left(x\right)\to \mathrm{Tr}\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)$$
2		r1tr	$$⊢\mathrm{Tr}{R}_1\left(x\right)$$
3	2	a1i	$$⊢x\in \mathrm{On}\to \mathrm{Tr}{R}_1\left(x\right)$$
4	1 3	mprg	$$⊢\mathrm{Tr}\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)$$
5		r1funlim	$$⊢\left(\mathrm{Fun}{R}_1\wedge \mathrm{Lim}\mathrm{dom}{R}_1\right)$$
6	5	simpli	$$⊢\mathrm{Fun}{R}_1$$
7		funiunfv	$$⊢\mathrm{Fun}{R}_1\to \bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
8	6 7	ax-mp	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
9		treq	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]\to \left(\mathrm{Tr}\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)\leftrightarrow \mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]\right)$$
10	8 9	ax-mp	$$⊢\mathrm{Tr}\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)\leftrightarrow \mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
11	4 10	mpbi	$$⊢\mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
12		trss	$$⊢\mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]\to \left(A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq \bigcup R_1\left[\mathrm{On}\right]\right)$$
13	11 12	ax-mp	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq \bigcup R_1\left[\mathrm{On}\right]$$