Theorem cusgrexilem1

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

	Ref	Expression
Hypothesis	usgrexi.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion	cusgrexilem1	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2		pwexg	⊢ ( 𝑉 ∈ 𝑊 → 𝒫 𝑉 ∈ V )
3	1 2	rabexd	⊢ ( 𝑉 ∈ 𝑊 → 𝑃 ∈ V )
4		resiexg	⊢ ( 𝑃 ∈ V → ( I ↾ 𝑃 ) ∈ V )
5	3 4	syl	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) ∈ V )