Theorem rtrclreclem1

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

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

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem1.1	$$⊢\phi \to R\in 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	1	elexd	$$⊢\phi \to R\in \mathrm{V}$$
17		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
18		ovex	$$⊢R{\uparrow }_{r}n\in \mathrm{V}$$
19	17 18	iunex	$$⊢\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
20	19	a1i	$$⊢\phi \to \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
21	12 15 16 20	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)$$
22	11 21	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)$$
23		df-rtrclrec	$$⊢\mathrm{t*rec}=\left(r\in \mathrm{V}⟼\bigcup _{n\in {\mathbb{N}}_0}\left(r{\uparrow }_{r}n\right)\right)$$
24		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)$$
25	24	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)$$
26	25	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)$$
27	23 26	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)$$
28	22 27	mpbir	$$⊢\phi \to R\subseteq \mathrm{t*rec}\left(R\right)$$