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		r1fun	$$⊢\mathrm{Fun}{R}_1$$
6		funiunfv	$$⊢\mathrm{Fun}{R}_1\to \bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
7	5 6	ax-mp	$$⊢\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)=\bigcup R_1\left[\mathrm{On}\right]$$
8		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)$$
9	7 8	ax-mp	$$⊢\mathrm{Tr}\bigcup _{x\in \mathrm{On}}{R}_1\left(x\right)\leftrightarrow \mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
10	4 9	mpbi	$$⊢\mathrm{Tr}\bigcup R_1\left[\mathrm{On}\right]$$
11		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)$$
12	10 11	ax-mp	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to A\subseteq \bigcup R_1\left[\mathrm{On}\right]$$