Theorem restsubel

Description: A subset belongs in the space it generates via restriction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	restsubel.1	$$⊢\phi \to J\in V$$
	restsubel.2	$$⊢\phi \to \bigcup J\in J$$
	restsubel.3	$$⊢\phi \to A\subseteq \bigcup J$$
Assertion	restsubel	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		restsubel.1	$$⊢\phi \to J\in V$$
2		restsubel.2	$$⊢\phi \to \bigcup J\in J$$
3		restsubel.3	$$⊢\phi \to A\subseteq \bigcup J$$
4		ineq1	$$⊢x=\bigcup J\to x\cap A=\bigcup J\cap A$$
5	4	eqeq2d	$$⊢x=\bigcup J\to \left(A=x\cap A\leftrightarrow A=\bigcup J\cap A\right)$$
6	5	adantl	$$⊢\left(\phi \wedge x=\bigcup J\right)\to \left(A=x\cap A\leftrightarrow A=\bigcup J\cap A\right)$$
7		incom	$$⊢\bigcup J\cap A=A\cap \bigcup J$$
8	7	a1i	$$⊢\phi \to \bigcup J\cap A=A\cap \bigcup J$$
9		df-ss	$$⊢A\subseteq \bigcup J\leftrightarrow A\cap \bigcup J=A$$
10	3 9	sylib	$$⊢\phi \to A\cap \bigcup J=A$$
11	8 10	eqtrd	$$⊢\phi \to \bigcup J\cap A=A$$
12	11	eqcomd	$$⊢\phi \to A=\bigcup J\cap A$$
13	2 6 12	rspcedvd	$$⊢\phi \to \exists x\in JA=x\cap A$$
14	2 3	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
15		elrest	$$⊢\left(J\in V\wedge A\in \mathrm{V}\right)\to \left(A\in \left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in JA=x\cap A\right)$$
16	1 14 15	syl2anc	$$⊢\phi \to \left(A\in \left(J{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists x\in JA=x\cap A\right)$$
17	13 16	mpbird	$$⊢\phi \to A\in \left(J{\upharpoonright }_{𝑡}A\right)$$