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 P = x 𝒫 V | x = 2
Assertion usgrexilem V W I P : dom I P 1-1 x 𝒫 V | x = 2

Proof

Step Hyp Ref Expression
1 usgrexi.p P = x 𝒫 V | x = 2
2 f1oi I P : P 1-1 onto P
3 f1of1 I P : P 1-1 onto P I P : P 1-1 P
4 2 3 ax-mp I P : P 1-1 P
5 dmresi dom I P = P
6 f1eq2 dom I P = P I P : dom I P 1-1 P I P : P 1-1 P
7 5 6 ax-mp I P : dom I P 1-1 P I P : P 1-1 P
8 4 7 mpbir I P : dom I P 1-1 P
9 1 eqcomi x 𝒫 V | x = 2 = P
10 f1eq3 x 𝒫 V | x = 2 = P I P : dom I P 1-1 x 𝒫 V | x = 2 I P : dom I P 1-1 P
11 9 10 mp1i V W I P : dom I P 1-1 x 𝒫 V | x = 2 I P : dom I P 1-1 P
12 8 11 mpbiri V W I P : dom I P 1-1 x 𝒫 V | x = 2