Theorem rtrclreclem2

Description: The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020)

	Ref	Expression
Hypothesis	rtrclreclem.ex	$$⊢\phi \to R\in \mathrm{V}$$
Assertion	rtrclreclem2	$$⊢\phi \to R\subseteq \mathrm{t*rec}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem.ex	$$⊢\phi \to R\in \mathrm{V}$$
2		1nn0	$$⊢1\in {\mathbb{N}}_0$$
3		ssidd	$$⊢\phi \to R\subseteq R$$
4	1	relexp1d	$$⊢\phi \to R{\uparrow }_{r}1=R$$
5	3 4	sseqtrrd	$$⊢\phi \to R\subseteq R{\uparrow }_{r}1$$
6		oveq2	$$⊢n=1\to R{\uparrow }_{r}n=R{\uparrow }_{r}1$$
7	6	sseq2d	$$⊢n=1\to \left(R\subseteq R{\uparrow }_{r}n\leftrightarrow R\subseteq R{\uparrow }_{r}1\right)$$
8	7	rspcev	$$⊢\left(1\in {\mathbb{N}}_0\wedge R\subseteq R{\uparrow }_{r}1\right)\to \exists n\in {\mathbb{N}}_{0}R\subseteq R{\uparrow }_{r}n$$
9	2 5 8	sylancr	$$⊢\phi \to \exists n\in {\mathbb{N}}_{0}R\subseteq R{\uparrow }_{r}n$$
10		ssiun	$$⊢\exists n\in {\mathbb{N}}_{0}R\subseteq R{\uparrow }_{r}n\to R\subseteq \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
11	9 10	syl	$$⊢\phi \to R\subseteq \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
12		eqidd	$$⊢\phi \to \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$
13		oveq1	$$⊢r=R\to r{\uparrow }_{r}n=R{\uparrow }_{r}n$$
14	13	iuneq2d	$$⊢r=R\to \bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
15	14	adantl	$$⊢\left(\phi \wedge r=R\right)\to \bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)=\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
16		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
17		ovex	$$⊢R{\uparrow }_{r}n\in \mathrm{V}$$
18	16 17	iunex	$$⊢\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
19	18	a1i	$$⊢\phi \to \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
20	12 15 1 19	fvmptd	$$⊢\phi \to \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)=\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
21	11 20	sseqtrrd	$$⊢\phi \to R\subseteq \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)$$
22		df-rtrclrec	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$
23		fveq1	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\to \mathrm{t*rec}\left(R\right)=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)$$
24	23	sseq2d	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\to \left(R\subseteq \mathrm{t*rec}\left(R\right)\leftrightarrow R\subseteq \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)\right)$$
25	24	imbi2d	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\to \left(\left(\phi \to R\subseteq \mathrm{t*rec}\left(R\right)\right)\leftrightarrow \left(\phi \to R\subseteq \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)\right)\right)$$
26	22 25	ax-mp	$$⊢\left(\phi \to R\subseteq \mathrm{t*rec}\left(R\right)\right)\leftrightarrow \left(\phi \to R\subseteq \left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)\left(R\right)\right)$$
27	21 26	mpbir	$$⊢\phi \to R\subseteq \mathrm{t*rec}\left(R\right)$$