Metamath Proof Explorer

Theorem ushgredgedg

Description: In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020)

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

Proof

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