Metamath Proof Explorer

Theorem sprsymrelfo

Description: The mapping F is a function from the subsets of the set of pairs over a fixed set V onto the symmetric relations R on the fixed set V . (Contributed by AV, 23-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 sprsymrelfo ⊢V∈W→F:P⟶ontoR

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 4 a1i ⊢V∈W→F:P⟶R
6 breq ⊢r=t→xry↔xty
7 breq ⊢r=t→yrx↔ytx
8 6 7 bibi12d ⊢r=t→xry↔yrx↔xty↔ytx
9 8 2ralbidv ⊢r=t→∀x∈V∀y∈Vxry↔yrx↔∀x∈V∀y∈Vxty↔ytx
10 9 2 elrab2 ⊢t∈R↔t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx
11 eqid ⊢q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb
12 11 sprsymrelfolem1 ⊢q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb∈𝒫Pairs⁡V
13 12 1 eleqtrri ⊢q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb∈P
14 13 a1i ⊢t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx∧V∈W→q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb∈P
15 rexeq ⊢f=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb→∃c∈fc=xy↔∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
16 15 opabbidv ⊢f=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb→xy|∃c∈fc=xy=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
17 16 eqeq2d ⊢f=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb→t=xy|∃c∈fc=xy↔t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
18 17 adantl ⊢t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx∧V∈W∧f=q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atb→t=xy|∃c∈fc=xy↔t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
19 velpw ⊢t∈𝒫V×V↔t⊆V×V
20 xpss ⊢V×V⊆V×V
21 sstr2 ⊢t⊆V×V→V×V⊆V×V→t⊆V×V
22 20 21 mpi ⊢t⊆V×V→t⊆V×V
23 df-rel ⊢Rel⁡t↔t⊆V×V
24 22 23 sylibr ⊢t⊆V×V→Rel⁡t
25 24 adantl ⊢V∈W∧t⊆V×V→Rel⁡t
26 dfrel4v ⊢Rel⁡t↔t=xy|xty
27 nfv ⊢ℲxV∈W∧t⊆V×V
28 nfra1 ⊢Ⅎx∀x∈V∀y∈Vxty↔ytx
29 27 28 nfan ⊢ℲxV∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx
30 nfv ⊢ℲyV∈W∧t⊆V×V
31 nfra2w ⊢Ⅎy∀x∈V∀y∈Vxty↔ytx
32 30 31 nfan ⊢ℲyV∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx
33 11 sprsymrelfolem2 ⊢V∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx→xty↔∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
34 33 3expa ⊢V∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx→xty↔∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
35 29 32 34 opabbid ⊢V∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx→xy|xty=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
36 35 eqeq2d ⊢V∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx→t=xy|xty↔t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
37 36 biimpd ⊢V∈W∧t⊆V×V∧∀x∈V∀y∈Vxty↔ytx→t=xy|xty→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
38 37 ex ⊢V∈W∧t⊆V×V→∀x∈V∀y∈Vxty↔ytx→t=xy|xty→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
39 38 com23 ⊢V∈W∧t⊆V×V→t=xy|xty→∀x∈V∀y∈Vxty↔ytx→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
40 26 39 biimtrid ⊢V∈W∧t⊆V×V→Rel⁡t→∀x∈V∀y∈Vxty↔ytx→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
41 25 40 mpd ⊢V∈W∧t⊆V×V→∀x∈V∀y∈Vxty↔ytx→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
42 41 expcom ⊢t⊆V×V→V∈W→∀x∈V∀y∈Vxty↔ytx→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
43 42 com23 ⊢t⊆V×V→∀x∈V∀y∈Vxty↔ytx→V∈W→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
44 19 43 sylbi ⊢t∈𝒫V×V→∀x∈V∀y∈Vxty↔ytx→V∈W→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
45 44 imp31 ⊢t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx∧V∈W→t=xy|∃c∈q∈Pairs⁡V|∀a∈V∀b∈Vq=ab→atbc=xy
46 14 18 45 rspcedvd ⊢t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx∧V∈W→∃f∈Pt=xy|∃c∈fc=xy
47 46 ex ⊢t∈𝒫V×V∧∀x∈V∀y∈Vxty↔ytx→V∈W→∃f∈Pt=xy|∃c∈fc=xy
48 10 47 sylbi ⊢t∈R→V∈W→∃f∈Pt=xy|∃c∈fc=xy
49 48 impcom ⊢V∈W∧t∈R→∃f∈Pt=xy|∃c∈fc=xy
50 1 2 3 sprsymrelfv ⊢f∈P→F⁡f=xy|∃c∈fc=xy
51 50 adantl ⊢V∈W∧t∈R∧f∈P→F⁡f=xy|∃c∈fc=xy
52 51 eqeq2d ⊢V∈W∧t∈R∧f∈P→t=F⁡f↔t=xy|∃c∈fc=xy
53 52 rexbidva ⊢V∈W∧t∈R→∃f∈Pt=F⁡f↔∃f∈Pt=xy|∃c∈fc=xy
54 49 53 mpbird ⊢V∈W∧t∈R→∃f∈Pt=F⁡f
55 54 ralrimiva ⊢V∈W→∀t∈R∃f∈Pt=F⁡f
56 dffo3 ⊢F:P⟶ontoR↔F:P⟶R∧∀t∈R∃f∈Pt=F⁡f
57 5 55 56 sylanbrc ⊢V∈W→F:P⟶ontoR