Metamath Proof Explorer

Theorem sprsymrelf1

Description: The mapping F is a one-to-one function from the subsets of the set of pairs over a fixed set V into the symmetric relations R on the fixed set V . (Contributed by AV, 19-Nov-2021)

Ref Expression
Hypotheses sprsymrelf.p ⊢P=𝒫Pairs⁡V
sprsymrelf.r ⊢R=r∈𝒫V×V|∀x∈V∀y∈Vxry↔yrx
sprsymrelf.f ⊢F=p∈P⟼xy|∃c∈pc=xy
Assertion sprsymrelf1 ⊢F:P⟶1-1R

Proof

Step Hyp Ref Expression
1 sprsymrelf.p ⊢P=𝒫Pairs⁡V
2 sprsymrelf.r ⊢R=r∈𝒫V×V|∀x∈V∀y∈Vxry↔yrx
3 sprsymrelf.f ⊢F=p∈P⟼xy|∃c∈pc=xy
4 1 2 3 sprsymrelf ⊢F:P⟶R
5 1 2 3 sprsymrelfv ⊢a∈P→F⁡a=xy|∃c∈ac=xy
6 1 2 3 sprsymrelfv ⊢b∈P→F⁡b=xy|∃c∈bc=xy
7 5 6 eqeqan12d ⊢a∈P∧b∈P→F⁡a=F⁡b↔xy|∃c∈ac=xy=xy|∃c∈bc=xy
8 1 eleq2i ⊢a∈P↔a∈𝒫Pairs⁡V
9 vex ⊢a∈V
10 9 elpw ⊢a∈𝒫Pairs⁡V↔a⊆Pairs⁡V
11 8 10 bitri ⊢a∈P↔a⊆Pairs⁡V
12 1 eleq2i ⊢b∈P↔b∈𝒫Pairs⁡V
13 vex ⊢b∈V
14 13 elpw ⊢b∈𝒫Pairs⁡V↔b⊆Pairs⁡V
15 12 14 bitri ⊢b∈P↔b⊆Pairs⁡V
16 sprsymrelf1lem ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V→xy|∃c∈ac=xy=xy|∃c∈bc=xy→a⊆b
17 16 imp ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V∧xy|∃c∈ac=xy=xy|∃c∈bc=xy→a⊆b
18 eqcom ⊢xy|∃c∈ac=xy=xy|∃c∈bc=xy↔xy|∃c∈bc=xy=xy|∃c∈ac=xy
19 sprsymrelf1lem ⊢b⊆Pairs⁡V∧a⊆Pairs⁡V→xy|∃c∈bc=xy=xy|∃c∈ac=xy→b⊆a
20 18 19 biimtrid ⊢b⊆Pairs⁡V∧a⊆Pairs⁡V→xy|∃c∈ac=xy=xy|∃c∈bc=xy→b⊆a
21 20 ancoms ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V→xy|∃c∈ac=xy=xy|∃c∈bc=xy→b⊆a
22 21 imp ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V∧xy|∃c∈ac=xy=xy|∃c∈bc=xy→b⊆a
23 17 22 eqssd ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V∧xy|∃c∈ac=xy=xy|∃c∈bc=xy→a=b
24 23 ex ⊢a⊆Pairs⁡V∧b⊆Pairs⁡V→xy|∃c∈ac=xy=xy|∃c∈bc=xy→a=b
25 11 15 24 syl2anb ⊢a∈P∧b∈P→xy|∃c∈ac=xy=xy|∃c∈bc=xy→a=b
26 7 25 sylbid ⊢a∈P∧b∈P→F⁡a=F⁡b→a=b
27 26 rgen2 ⊢∀a∈P∀b∈PF⁡a=F⁡b→a=b
28 dff13 ⊢F:P⟶1-1R↔F:P⟶R∧∀a∈P∀b∈PF⁡a=F⁡b→a=b
29 4 27 28 mpbir2an ⊢F:P⟶1-1R