Metamath Proof Explorer

Theorem ushgredgedgloop

Description: In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex N and the set of loops at this vertex N . (Contributed by AV, 11-Dec-2020) (Revised by AV, 6-Jul-2022)

Ref Expression
Hypotheses ushgredgedgloop.e 
|- E = ( Edg ` G )
ushgredgedgloop.i 
|- I = ( iEdg ` G )
ushgredgedgloop.a 
|- A = { i e. dom I | ( I ` i ) = { N } }
ushgredgedgloop.b 
|- B = { e e. E | e = { N } }
ushgredgedgloop.f 
|- F = ( x e. A |-> ( I ` x ) )
Assertion ushgredgedgloop 
|- ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )

Proof

Step Hyp Ref Expression
1 ushgredgedgloop.e 
 |-  E = ( Edg ` G )
2 ushgredgedgloop.i 
 |-  I = ( iEdg ` G )
3 ushgredgedgloop.a 
 |-  A = { i e. dom I | ( I ` i ) = { N } }
4 ushgredgedgloop.b 
 |-  B = { e e. E | e = { N } }
5 ushgredgedgloop.f 
 |-  F = ( x e. A |-> ( I ` x ) )
6 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
7 6 2 ushgrf 
 |-  ( G e. USHGraph -> I : dom I -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) )
8 7 adantr 
 |-  ( ( G e. USHGraph /\ N e. V ) -> I : dom I -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) )
9 ssrab2 
 |-  { i e. dom I | ( I ` i ) = { N } } C_ dom I
10 f1ores 
 |-  ( ( I : dom I -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) /\ { i e. dom I | ( I ` i ) = { N } } C_ dom I ) -> ( I |` { i e. dom I | ( I ` i ) = { N } } ) : { i e. dom I | ( I ` i ) = { N } } -1-1-onto-> ( I " { i e. dom I | ( I ` i ) = { N } } ) )
11 8 9 10 sylancl 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( I |` { i e. dom I | ( I ` i ) = { N } } ) : { i e. dom I | ( I ` i ) = { N } } -1-1-onto-> ( I " { i e. dom I | ( I ` i ) = { N } } ) )
12 3 a1i 
 |-  ( ( G e. USHGraph /\ N e. V ) -> A = { i e. dom I | ( I ` i ) = { N } } )
13 eqidd 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ x e. A ) -> ( I ` x ) = ( I ` x ) )
14 12 13 mpteq12dva 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( x e. A |-> ( I ` x ) ) = ( x e. { i e. dom I | ( I ` i ) = { N } } |-> ( I ` x ) ) )
15 5 14 syl5eq 
 |-  ( ( G e. USHGraph /\ N e. V ) -> F = ( x e. { i e. dom I | ( I ` i ) = { N } } |-> ( I ` x ) ) )
16 f1f 
 |-  ( I : dom I -1-1-> ( ~P ( Vtx ` G ) \ { (/) } ) -> I : dom I --> ( ~P ( Vtx ` G ) \ { (/) } ) )
17 7 16 syl 
 |-  ( G e. USHGraph -> I : dom I --> ( ~P ( Vtx ` G ) \ { (/) } ) )
18 9 a1i 
 |-  ( G e. USHGraph -> { i e. dom I | ( I ` i ) = { N } } C_ dom I )
19 17 18 feqresmpt 
 |-  ( G e. USHGraph -> ( I |` { i e. dom I | ( I ` i ) = { N } } ) = ( x e. { i e. dom I | ( I ` i ) = { N } } |-> ( I ` x ) ) )
20 19 adantr 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( I |` { i e. dom I | ( I ` i ) = { N } } ) = ( x e. { i e. dom I | ( I ` i ) = { N } } |-> ( I ` x ) ) )
21 15 20 eqtr4d 
 |-  ( ( G e. USHGraph /\ N e. V ) -> F = ( I |` { i e. dom I | ( I ` i ) = { N } } ) )
22 ushgruhgr 
 |-  ( G e. USHGraph -> G e. UHGraph )
23 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
24 23 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
25 22 24 syl 
 |-  ( G e. USHGraph -> Fun ( iEdg ` G ) )
26 2 funeqi 
 |-  ( Fun I <-> Fun ( iEdg ` G ) )
27 25 26 sylibr 
 |-  ( G e. USHGraph -> Fun I )
28 27 adantr 
 |-  ( ( G e. USHGraph /\ N e. V ) -> Fun I )
29 dfimafn 
 |-  ( ( Fun I /\ { i e. dom I | ( I ` i ) = { N } } C_ dom I ) -> ( I " { i e. dom I | ( I ` i ) = { N } } ) = { e | E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e } )
30 28 9 29 sylancl 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( I " { i e. dom I | ( I ` i ) = { N } } ) = { e | E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e } )
31 fveqeq2 
 |-  ( i = j -> ( ( I ` i ) = { N } <-> ( I ` j ) = { N } ) )
32 31 elrab 
 |-  ( j e. { i e. dom I | ( I ` i ) = { N } } <-> ( j e. dom I /\ ( I ` j ) = { N } ) )
33 simpl 
 |-  ( ( j e. dom I /\ ( I ` j ) = { N } ) -> j e. dom I )
34 fvelrn 
 |-  ( ( Fun I /\ j e. dom I ) -> ( I ` j ) e. ran I )
35 2 eqcomi 
 |-  ( iEdg ` G ) = I
36 35 rneqi 
 |-  ran ( iEdg ` G ) = ran I
37 34 36 eleqtrrdi 
 |-  ( ( Fun I /\ j e. dom I ) -> ( I ` j ) e. ran ( iEdg ` G ) )
38 28 33 37 syl2an 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) ) -> ( I ` j ) e. ran ( iEdg ` G ) )
39 38 3adant3 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> ( I ` j ) e. ran ( iEdg ` G ) )
40 eleq1 
 |-  ( f = ( I ` j ) -> ( f e. ran ( iEdg ` G ) <-> ( I ` j ) e. ran ( iEdg ` G ) ) )
41 40 eqcoms 
 |-  ( ( I ` j ) = f -> ( f e. ran ( iEdg ` G ) <-> ( I ` j ) e. ran ( iEdg ` G ) ) )
42 41 3ad2ant3 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> ( f e. ran ( iEdg ` G ) <-> ( I ` j ) e. ran ( iEdg ` G ) ) )
43 39 42 mpbird 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> f e. ran ( iEdg ` G ) )
44 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
45 44 a1i 
 |-  ( G e. USHGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
46 1 45 syl5eq 
 |-  ( G e. USHGraph -> E = ran ( iEdg ` G ) )
47 46 eleq2d 
 |-  ( G e. USHGraph -> ( f e. E <-> f e. ran ( iEdg ` G ) ) )
48 47 adantr 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( f e. E <-> f e. ran ( iEdg ` G ) ) )
49 48 3ad2ant1 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> ( f e. E <-> f e. ran ( iEdg ` G ) ) )
50 43 49 mpbird 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> f e. E )
51 eqeq1 
 |-  ( ( I ` j ) = f -> ( ( I ` j ) = { N } <-> f = { N } ) )
52 51 biimpcd 
 |-  ( ( I ` j ) = { N } -> ( ( I ` j ) = f -> f = { N } ) )
53 52 adantl 
 |-  ( ( j e. dom I /\ ( I ` j ) = { N } ) -> ( ( I ` j ) = f -> f = { N } ) )
54 53 a1i 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( ( j e. dom I /\ ( I ` j ) = { N } ) -> ( ( I ` j ) = f -> f = { N } ) ) )
55 54 3imp 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> f = { N } )
56 50 55 jca 
 |-  ( ( ( G e. USHGraph /\ N e. V ) /\ ( j e. dom I /\ ( I ` j ) = { N } ) /\ ( I ` j ) = f ) -> ( f e. E /\ f = { N } ) )
57 56 3exp 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( ( j e. dom I /\ ( I ` j ) = { N } ) -> ( ( I ` j ) = f -> ( f e. E /\ f = { N } ) ) ) )
58 32 57 syl5bi 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( j e. { i e. dom I | ( I ` i ) = { N } } -> ( ( I ` j ) = f -> ( f e. E /\ f = { N } ) ) ) )
59 58 rexlimdv 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f -> ( f e. E /\ f = { N } ) ) )
60 25 funfnd 
 |-  ( G e. USHGraph -> ( iEdg ` G ) Fn dom ( iEdg ` G ) )
61 fvelrnb 
 |-  ( ( iEdg ` G ) Fn dom ( iEdg ` G ) -> ( f e. ran ( iEdg ` G ) <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = f ) )
62 60 61 syl 
 |-  ( G e. USHGraph -> ( f e. ran ( iEdg ` G ) <-> E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = f ) )
63 35 dmeqi 
 |-  dom ( iEdg ` G ) = dom I
64 63 eleq2i 
 |-  ( j e. dom ( iEdg ` G ) <-> j e. dom I )
65 64 biimpi 
 |-  ( j e. dom ( iEdg ` G ) -> j e. dom I )
66 65 adantr 
 |-  ( ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) -> j e. dom I )
67 66 adantl 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> j e. dom I )
68 35 fveq1i 
 |-  ( ( iEdg ` G ) ` j ) = ( I ` j )
69 68 eqeq2i 
 |-  ( f = ( ( iEdg ` G ) ` j ) <-> f = ( I ` j ) )
70 69 biimpi 
 |-  ( f = ( ( iEdg ` G ) ` j ) -> f = ( I ` j ) )
71 70 eqcoms 
 |-  ( ( ( iEdg ` G ) ` j ) = f -> f = ( I ` j ) )
72 71 eqeq1d 
 |-  ( ( ( iEdg ` G ) ` j ) = f -> ( f = { N } <-> ( I ` j ) = { N } ) )
73 72 biimpcd 
 |-  ( f = { N } -> ( ( ( iEdg ` G ) ` j ) = f -> ( I ` j ) = { N } ) )
74 73 adantl 
 |-  ( ( G e. USHGraph /\ f = { N } ) -> ( ( ( iEdg ` G ) ` j ) = f -> ( I ` j ) = { N } ) )
75 74 adantld 
 |-  ( ( G e. USHGraph /\ f = { N } ) -> ( ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) -> ( I ` j ) = { N } ) )
76 75 imp 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> ( I ` j ) = { N } )
77 67 76 jca 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> ( j e. dom I /\ ( I ` j ) = { N } ) )
78 77 32 sylibr 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> j e. { i e. dom I | ( I ` i ) = { N } } )
79 68 eqeq1i 
 |-  ( ( ( iEdg ` G ) ` j ) = f <-> ( I ` j ) = f )
80 79 biimpi 
 |-  ( ( ( iEdg ` G ) ` j ) = f -> ( I ` j ) = f )
81 80 adantl 
 |-  ( ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) -> ( I ` j ) = f )
82 81 adantl 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> ( I ` j ) = f )
83 78 82 jca 
 |-  ( ( ( G e. USHGraph /\ f = { N } ) /\ ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) ) -> ( j e. { i e. dom I | ( I ` i ) = { N } } /\ ( I ` j ) = f ) )
84 83 ex 
 |-  ( ( G e. USHGraph /\ f = { N } ) -> ( ( j e. dom ( iEdg ` G ) /\ ( ( iEdg ` G ) ` j ) = f ) -> ( j e. { i e. dom I | ( I ` i ) = { N } } /\ ( I ` j ) = f ) ) )
85 84 reximdv2 
 |-  ( ( G e. USHGraph /\ f = { N } ) -> ( E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = f -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) )
86 85 ex 
 |-  ( G e. USHGraph -> ( f = { N } -> ( E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = f -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) ) )
87 86 com23 
 |-  ( G e. USHGraph -> ( E. j e. dom ( iEdg ` G ) ( ( iEdg ` G ) ` j ) = f -> ( f = { N } -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) ) )
88 62 87 sylbid 
 |-  ( G e. USHGraph -> ( f e. ran ( iEdg ` G ) -> ( f = { N } -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) ) )
89 47 88 sylbid 
 |-  ( G e. USHGraph -> ( f e. E -> ( f = { N } -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) ) )
90 89 impd 
 |-  ( G e. USHGraph -> ( ( f e. E /\ f = { N } ) -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) )
91 90 adantr 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( ( f e. E /\ f = { N } ) -> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) )
92 59 91 impbid 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f <-> ( f e. E /\ f = { N } ) ) )
93 vex 
 |-  f e. _V
94 eqeq2 
 |-  ( e = f -> ( ( I ` j ) = e <-> ( I ` j ) = f ) )
95 94 rexbidv 
 |-  ( e = f -> ( E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e <-> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f ) )
96 93 95 elab 
 |-  ( f e. { e | E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e } <-> E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = f )
97 eqeq1 
 |-  ( e = f -> ( e = { N } <-> f = { N } ) )
98 97 4 elrab2 
 |-  ( f e. B <-> ( f e. E /\ f = { N } ) )
99 92 96 98 3bitr4g 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( f e. { e | E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e } <-> f e. B ) )
100 99 eqrdv 
 |-  ( ( G e. USHGraph /\ N e. V ) -> { e | E. j e. { i e. dom I | ( I ` i ) = { N } } ( I ` j ) = e } = B )
101 30 100 eqtr2d 
 |-  ( ( G e. USHGraph /\ N e. V ) -> B = ( I " { i e. dom I | ( I ` i ) = { N } } ) )
102 21 12 101 f1oeq123d 
 |-  ( ( G e. USHGraph /\ N e. V ) -> ( F : A -1-1-onto-> B <-> ( I |` { i e. dom I | ( I ` i ) = { N } } ) : { i e. dom I | ( I ` i ) = { N } } -1-1-onto-> ( I " { i e. dom I | ( I ` i ) = { N } } ) ) )
103 11 102 mpbird 
 |-  ( ( G e. USHGraph /\ N e. V ) -> F : A -1-1-onto-> B )