This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )