Theorem usgrexilem

Description: Lemma for usgrexi . (Contributed by AV, 12-Jan-2018) (Revised by AV, 10-Nov-2021)

	Ref	Expression
Hypothesis	usgrexi.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion	usgrexilem	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2		f1oi	⊢ ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃
3		f1of1	⊢ ( ( I ↾ 𝑃 ) : 𝑃 –1-1-onto→ 𝑃 → ( I ↾ 𝑃 ) : 𝑃 –1-1→ 𝑃 )
4	2 3	ax-mp	⊢ ( I ↾ 𝑃 ) : 𝑃 –1-1→ 𝑃
5		dmresi	⊢ dom ( I ↾ 𝑃 ) = 𝑃
6		f1eq2	⊢ ( dom ( I ↾ 𝑃 ) = 𝑃 → ( ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ 𝑃 ↔ ( I ↾ 𝑃 ) : 𝑃 –1-1→ 𝑃 ) )
7	5 6	ax-mp	⊢ ( ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ 𝑃 ↔ ( I ↾ 𝑃 ) : 𝑃 –1-1→ 𝑃 )
8	4 7	mpbir	⊢ ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ 𝑃
9	1	eqcomi	⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = 𝑃
10		f1eq3	⊢ ( { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } = 𝑃 → ( ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ 𝑃 ) )
11	9 10	mp1i	⊢ ( 𝑉 ∈ 𝑊 → ( ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ 𝑃 ) )
12	8 11	mpbiri	⊢ ( 𝑉 ∈ 𝑊 → ( I ↾ 𝑃 ) : dom ( I ↾ 𝑃 ) –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )