Metamath Proof Explorer


Theorem uspgrsprfo

Description: The mapping F is a function from the "simple pseudographs" with a fixed set of vertices V onto the subsets of the set of pairs over the set V . (Contributed by AV, 25-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p P = 𝒫 Pairs V
uspgrsprf.g G = v e | v = V q USHGraph Vtx q = v Edg q = e
uspgrsprf.f F = g G 2 nd g
Assertion uspgrsprfo V W F : G onto P

Proof

Step Hyp Ref Expression
1 uspgrsprf.p P = 𝒫 Pairs V
2 uspgrsprf.g G = v e | v = V q USHGraph Vtx q = v Edg q = e
3 uspgrsprf.f F = g G 2 nd g
4 1 2 3 uspgrsprf F : G P
5 4 a1i V W F : G P
6 1 eleq2i a P a 𝒫 Pairs V
7 velpw a 𝒫 Pairs V a Pairs V
8 6 7 bitri a P a Pairs V
9 eqidd a Pairs V V W V = V
10 vex a V
11 10 a1i a Pairs V V W a V
12 f1oi I a : a 1-1 onto a
13 12 a1i a Pairs V V W I a : a 1-1 onto a
14 dmresi dom I a = a
15 f1oeq2 dom I a = a I a : dom I a 1-1 onto a I a : a 1-1 onto a
16 14 15 ax-mp I a : dom I a 1-1 onto a I a : a 1-1 onto a
17 13 16 sylibr a Pairs V V W I a : dom I a 1-1 onto a
18 sprvalpwle2 V W Pairs V = p 𝒫 V | p 2
19 18 sseq2d V W a Pairs V a p 𝒫 V | p 2
20 19 biimpac a Pairs V V W a p 𝒫 V | p 2
21 17 20 jca a Pairs V V W I a : dom I a 1-1 onto a a p 𝒫 V | p 2
22 f1oeq3 f = a I a : dom I a 1-1 onto f I a : dom I a 1-1 onto a
23 sseq1 f = a f p 𝒫 V | p 2 a p 𝒫 V | p 2
24 22 23 anbi12d f = a I a : dom I a 1-1 onto f f p 𝒫 V | p 2 I a : dom I a 1-1 onto a a p 𝒫 V | p 2
25 11 21 24 elabd a Pairs V V W f I a : dom I a 1-1 onto f f p 𝒫 V | p 2
26 resiexg a V I a V
27 10 26 ax-mp I a V
28 27 f11o I a : dom I a 1-1 p 𝒫 V | p 2 f I a : dom I a 1-1 onto f f p 𝒫 V | p 2
29 25 28 sylibr a Pairs V V W I a : dom I a 1-1 p 𝒫 V | p 2
30 10 a1i a Pairs V a V
31 30 resiexd a Pairs V I a V
32 31 anim2i V W a Pairs V V W I a V
33 32 ancoms a Pairs V V W V W I a V
34 isuspgrop V W I a V V I a USHGraph I a : dom I a 1-1 p 𝒫 V | p 2
35 33 34 syl a Pairs V V W V I a USHGraph I a : dom I a 1-1 p 𝒫 V | p 2
36 29 35 mpbird a Pairs V V W V I a USHGraph
37 fveqeq2 q = V I a Vtx q = V Vtx V I a = V
38 fveqeq2 q = V I a Edg q = a Edg V I a = a
39 37 38 anbi12d q = V I a Vtx q = V Edg q = a Vtx V I a = V Edg V I a = a
40 39 adantl a Pairs V V W q = V I a Vtx q = V Edg q = a Vtx V I a = V Edg V I a = a
41 opvtxfv V W I a V Vtx V I a = V
42 32 41 syl V W a Pairs V Vtx V I a = V
43 edgopval V W I a V Edg V I a = ran I a
44 32 43 syl V W a Pairs V Edg V I a = ran I a
45 rnresi ran I a = a
46 44 45 syl6eq V W a Pairs V Edg V I a = a
47 42 46 jca V W a Pairs V Vtx V I a = V Edg V I a = a
48 47 ancoms a Pairs V V W Vtx V I a = V Edg V I a = a
49 36 40 48 rspcedvd a Pairs V V W q USHGraph Vtx q = V Edg q = a
50 9 49 jca a Pairs V V W V = V q USHGraph Vtx q = V Edg q = a
51 2 eleq2i V a G V a v e | v = V q USHGraph Vtx q = v Edg q = e
52 30 anim1i a Pairs V V W a V V W
53 52 ancomd a Pairs V V W V W a V
54 eqeq1 v = V v = V V = V
55 54 adantr v = V e = a v = V V = V
56 eqeq2 v = V Vtx q = v Vtx q = V
57 eqeq2 e = a Edg q = e Edg q = a
58 56 57 bi2anan9 v = V e = a Vtx q = v Edg q = e Vtx q = V Edg q = a
59 58 rexbidv v = V e = a q USHGraph Vtx q = v Edg q = e q USHGraph Vtx q = V Edg q = a
60 55 59 anbi12d v = V e = a v = V q USHGraph Vtx q = v Edg q = e V = V q USHGraph Vtx q = V Edg q = a
61 60 opelopabga V W a V V a v e | v = V q USHGraph Vtx q = v Edg q = e V = V q USHGraph Vtx q = V Edg q = a
62 53 61 syl a Pairs V V W V a v e | v = V q USHGraph Vtx q = v Edg q = e V = V q USHGraph Vtx q = V Edg q = a
63 51 62 syl5bb a Pairs V V W V a G V = V q USHGraph Vtx q = V Edg q = a
64 50 63 mpbird a Pairs V V W V a G
65 fveq2 b = V a 2 nd b = 2 nd V a
66 65 eqeq2d b = V a a = 2 nd b a = 2 nd V a
67 66 adantl a Pairs V V W b = V a a = 2 nd b a = 2 nd V a
68 op2ndg V W a V 2 nd V a = a
69 68 elvd V W 2 nd V a = a
70 69 adantl a Pairs V V W 2 nd V a = a
71 70 eqcomd a Pairs V V W a = 2 nd V a
72 64 67 71 rspcedvd a Pairs V V W b G a = 2 nd b
73 72 ex a Pairs V V W b G a = 2 nd b
74 8 73 sylbi a P V W b G a = 2 nd b
75 74 impcom V W a P b G a = 2 nd b
76 1 2 3 uspgrsprfv b G F b = 2 nd b
77 76 adantl V W a P b G F b = 2 nd b
78 77 eqeq2d V W a P b G a = F b a = 2 nd b
79 78 rexbidva V W a P b G a = F b b G a = 2 nd b
80 75 79 mpbird V W a P b G a = F b
81 80 ralrimiva V W a P b G a = F b
82 dffo3 F : G onto P F : G P a P b G a = F b
83 5 81 82 sylanbrc V W F : G onto P