Theorem cusgrexilem1

Description: Lemma 1 for cusgrexi . (Contributed by Alexander van der Vekens, 12-Jan-2018)

	Ref	Expression
Hypothesis	usgrexi.p	$$⊢P=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
Assertion	cusgrexilem1	$$⊢V\in W\to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	$$⊢P=\left\{x\in 𝒫V|\left|x\right|=2\right\}$$
2		pwexg	$$⊢V\in W\to 𝒫V\in \mathrm{V}$$
3	1 2	rabexd	$$⊢V\in W\to P\in \mathrm{V}$$
4		resiexg	$$⊢P\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$
5	3 4	syl	$$⊢V\in W\to {\mathrm{I}\upharpoonright }_P\in \mathrm{V}$$