Metamath Proof Explorer

Theorem uspgrbisymrelALT

Description: Alternate proof of uspgrbisymrel not using the definition of equinumerosity. (Contributed by AV, 26-Nov-2021) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses uspgrbisymrel.g ⊢G=ve|v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e
uspgrbisymrel.r ⊢R=r∈𝒫V×V|∀x∈V∀y∈Vxry↔yrx
Assertion uspgrbisymrelALT ⊢V∈W→∃ff:G⟶1-1 ontoR

Proof

Step Hyp Ref Expression
1 uspgrbisymrel.g ⊢G=ve|v=V∧∃q∈USHGraphVtx⁡q=v∧Edg⁡q=e
2 uspgrbisymrel.r ⊢R=r∈𝒫V×V|∀x∈V∀y∈Vxry↔yrx
3 fvex ⊢Pairs⁡V∈V
4 3 pwex ⊢𝒫Pairs⁡V∈V
5 mptexg ⊢𝒫Pairs⁡V∈V→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∈V
6 4 5 mp1i ⊢V∈W→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∈V
7 eqid ⊢𝒫Pairs⁡V=𝒫Pairs⁡V
8 7 1 uspgrex ⊢V∈W→G∈V
9 mptexg ⊢G∈V→g∈G⟼2nd⁡g∈V
10 8 9 syl ⊢V∈W→g∈G⟼2nd⁡g∈V
11 coexg ⊢p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∈V∧g∈G⟼2nd⁡g∈V→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g∈V
12 6 10 11 syl2anc ⊢V∈W→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g∈V
13 eqid ⊢p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy=p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy
14 7 2 13 sprsymrelf1o ⊢V∈W→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy:𝒫Pairs⁡V⟶1-1 ontoR
15 eqid ⊢g∈G⟼2nd⁡g=g∈G⟼2nd⁡g
16 7 1 15 uspgrsprf1o ⊢V∈W→g∈G⟼2nd⁡g:G⟶1-1 onto𝒫Pairs⁡V
17 f1oco ⊢p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy:𝒫Pairs⁡V⟶1-1 ontoR∧g∈G⟼2nd⁡g:G⟶1-1 onto𝒫Pairs⁡V→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g:G⟶1-1 ontoR
18 14 16 17 syl2anc ⊢V∈W→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g:G⟶1-1 ontoR
19 f1oeq1 ⊢f=p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g→f:G⟶1-1 ontoR↔p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g:G⟶1-1 ontoR
20 19 spcegv ⊢p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g∈V→p∈𝒫Pairs⁡V⟼xy|∃c∈pc=xy∘g∈G⟼2nd⁡g:G⟶1-1 ontoR→∃ff:G⟶1-1 ontoR
21 12 18 20 sylc ⊢V∈W→∃ff:G⟶1-1 ontoR