Theorem rtrclreclem2

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

	Ref	Expression
Hypotheses	rtrclreclem2.1	$$⊢\phi \to \mathrm{Rel}R$$
	rtrclreclem2.2	$$⊢\phi \to R\in V$$
Assertion	rtrclreclem2	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*rec}\left(R\right)$$

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem2.1	$$⊢\phi \to \mathrm{Rel}R$$
2		rtrclreclem2.2	$$⊢\phi \to R\in V$$
3		0nn0	$$⊢0\in {\mathbb{N}}_0$$
4		ssid	$$⊢{\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
5	1 2	relexp0d	$$⊢\phi \to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}$$
6	4 5	sseqtrrid	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}0$$
7		oveq2	$$⊢n=0\to R{\uparrow }_{r}n=R{\uparrow }_{r}0$$
8	7	sseq2d	$$⊢n=0\to \left({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}n\leftrightarrow {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}0\right)$$
9	8	rspcev	$$⊢\left(0\in {\mathbb{N}}_0\wedge {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}0\right)\to \exists n\in {\mathbb{N}}_0{\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}n$$
10	3 6 9	sylancr	$$⊢\phi \to \exists n\in {\mathbb{N}}_0{\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}n$$
11		ssiun	$$⊢\exists n\in {\mathbb{N}}_0{\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq R{\uparrow }_{r}n\to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
12	10 11	syl	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)$$
13	2	elexd	$$⊢\phi \to R\in \mathrm{V}$$
14		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
15		ovex	$$⊢R{\uparrow }_{r}n\in \mathrm{V}$$
16	14 15	iunex	$$⊢\bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}$$
17		oveq1	$$⊢r=R\to r{\uparrow }_{r}n=R{\uparrow }_{r}n$$
18	17	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)$$
19		eqid	$$⊢\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)$$
20	18 19	fvmptg	$$⊢\left(R\in \mathrm{V}\wedge \bigcup _{n\in {\mathbb{N}}_0}\left(R{\uparrow }_{r}n\right)\in \mathrm{V}\right)\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	13 16 20	sylancl	$$⊢\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	12 21	sseqtrrd	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup 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({\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*rec}\left(R\right)\leftrightarrow {\mathrm{I}\upharpoonright }_{\bigcup \bigcup 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 {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*rec}\left(R\right)\right)\leftrightarrow \left(\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup 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 {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*rec}\left(R\right)\right)\leftrightarrow \left(\phi \to {\mathrm{I}\upharpoonright }_{\bigcup \bigcup 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 {\mathrm{I}\upharpoonright }_{\bigcup \bigcup R}\subseteq \mathrm{t*rec}\left(R\right)$$