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 ⊢ 𝐸 = ( Edg ‘ 𝐺 )
ushgredgedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
ushgredgedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
ushgredgedg.a ⊢ 𝐴 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) }
ushgredgedg.b ⊢ 𝐵 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
ushgredgedg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐼 ‘ 𝑥 ) )
Assertion ushgredgedg ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 ushgredgedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 ushgredgedg.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 ushgredgedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
4 ushgredgedg.a ⊢ 𝐴 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) }
5 ushgredgedg.b ⊢ 𝐵 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 }
6 ushgredgedg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐼 ‘ 𝑥 ) )
7 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
8 7 2 ushgrf ⊢ ( 𝐺 ∈ USHGraph → 𝐼 : dom 𝐼 –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
9 8 adantr ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐼 : dom 𝐼 –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
10 ssrab2 ⊢ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ⊆ dom 𝐼
11 f1ores ⊢ ( ( 𝐼 : dom 𝐼 –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ∧ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ⊆ dom 𝐼 ) → ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) : { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } –1-1-onto→ ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) )
12 9 10 11 sylancl ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) : { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } –1-1-onto→ ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) )
13 4 a1i ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐴 = { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } )
14 eqidd ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑥 ) )
15 13 14 mpteq12dva ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑥 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↦ ( 𝐼 ‘ 𝑥 ) ) )
16 6 15 eqtrid ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 = ( 𝑥 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↦ ( 𝐼 ‘ 𝑥 ) ) )
17 f1f ⊢ ( 𝐼 : dom 𝐼 –1-1→ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → 𝐼 : dom 𝐼 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
18 8 17 syl ⊢ ( 𝐺 ∈ USHGraph → 𝐼 : dom 𝐼 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
19 10 a1i ⊢ ( 𝐺 ∈ USHGraph → { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ⊆ dom 𝐼 )
20 18 19 feqresmpt ⊢ ( 𝐺 ∈ USHGraph → ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) = ( 𝑥 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↦ ( 𝐼 ‘ 𝑥 ) ) )
21 20 adantr ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) = ( 𝑥 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↦ ( 𝐼 ‘ 𝑥 ) ) )
22 21 eqcomd ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑥 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↦ ( 𝐼 ‘ 𝑥 ) ) = ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) )
23 16 22 eqtrd ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 = ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) )
24 ushgruhgr ⊢ ( 𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph )
25 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
26 25 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
27 24 26 syl ⊢ ( 𝐺 ∈ USHGraph → Fun ( iEdg ‘ 𝐺 ) )
28 2 funeqi ⊢ ( Fun 𝐼 ↔ Fun ( iEdg ‘ 𝐺 ) )
29 27 28 sylibr ⊢ ( 𝐺 ∈ USHGraph → Fun 𝐼 )
30 29 adantr ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → Fun 𝐼 )
31 dfimafn ⊢ ( ( Fun 𝐼 ∧ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ⊆ dom 𝐼 ) → ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) = { 𝑒 ∣ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 } )
32 30 10 31 sylancl ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) = { 𝑒 ∣ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 } )
33 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝐼 ‘ 𝑖 ) = ( 𝐼 ‘ 𝑗 ) )
34 33 eleq2d ⊢ ( 𝑖 = 𝑗 → ( 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) ↔ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
35 34 elrab ⊢ ( 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ↔ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
36 simpl ⊢ ( ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) → 𝑗 ∈ dom 𝐼 )
37 fvelrn ⊢ ( ( Fun 𝐼 ∧ 𝑗 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑗 ) ∈ ran 𝐼 )
38 2 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
39 38 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
40 39 eleq2i ⊢ ( ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) ↔ ( 𝐼 ‘ 𝑗 ) ∈ ran 𝐼 )
41 37 40 sylibr ⊢ ( ( Fun 𝐼 ∧ 𝑗 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) )
42 30 36 41 syl2an ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ) → ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) )
43 42 3adant3 ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) )
44 eleq1 ⊢ ( 𝑓 = ( 𝐼 ‘ 𝑗 ) → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
45 44 eqcoms ⊢ ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
46 45 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ( 𝐼 ‘ 𝑗 ) ∈ ran ( iEdg ‘ 𝐺 ) ) )
47 43 46 mpbird ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) )
48 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
49 48 a1i ⊢ ( 𝐺 ∈ USHGraph → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
50 1 49 eqtrid ⊢ ( 𝐺 ∈ USHGraph → 𝐸 = ran ( iEdg ‘ 𝐺 ) )
51 50 eleq2d ⊢ ( 𝐺 ∈ USHGraph → ( 𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ) )
52 51 adantr ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ) )
53 52 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → ( 𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ) )
54 47 53 mpbird ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → 𝑓 ∈ 𝐸 )
55 eleq2 ⊢ ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → ( 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ↔ 𝑁 ∈ 𝑓 ) )
56 55 biimpcd ⊢ ( 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) → ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → 𝑁 ∈ 𝑓 ) )
57 56 adantl ⊢ ( ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) → ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → 𝑁 ∈ 𝑓 ) )
58 57 a1i ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) → ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → 𝑁 ∈ 𝑓 ) ) )
59 58 3imp ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → 𝑁 ∈ 𝑓 )
60 54 59 jca ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) → ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) )
61 60 3exp ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) → ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) ) ) )
62 35 61 biimtrid ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } → ( ( 𝐼 ‘ 𝑗 ) = 𝑓 → ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) ) ) )
63 62 rexlimdv ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 → ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) ) )
64 27 funfnd ⊢ ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
65 fvelrnb ⊢ ( ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) )
66 64 65 syl ⊢ ( 𝐺 ∈ USHGraph → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) ↔ ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) )
67 38 dmeqi ⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐼
68 67 eleq2i ⊢ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ↔ 𝑗 ∈ dom 𝐼 )
69 68 biimpi ⊢ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) → 𝑗 ∈ dom 𝐼 )
70 69 adantr ⊢ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) → 𝑗 ∈ dom 𝐼 )
71 70 adantl ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → 𝑗 ∈ dom 𝐼 )
72 38 fveq1i ⊢ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = ( 𝐼 ‘ 𝑗 )
73 72 eqeq2i ⊢ ( 𝑓 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) ↔ 𝑓 = ( 𝐼 ‘ 𝑗 ) )
74 73 biimpi ⊢ ( 𝑓 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) → 𝑓 = ( 𝐼 ‘ 𝑗 ) )
75 74 eqcoms ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → 𝑓 = ( 𝐼 ‘ 𝑗 ) )
76 75 eleq2d ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → ( 𝑁 ∈ 𝑓 ↔ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
77 76 biimpcd ⊢ ( 𝑁 ∈ 𝑓 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
78 77 adantl ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
79 78 adantld ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) → ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) → 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
80 79 imp ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) )
81 71 80 jca ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → ( 𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ ( 𝐼 ‘ 𝑗 ) ) )
82 81 35 sylibr ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } )
83 72 eqeq1i ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ↔ ( 𝐼 ‘ 𝑗 ) = 𝑓 )
84 83 biimpi ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → ( 𝐼 ‘ 𝑗 ) = 𝑓 )
85 84 adantl ⊢ ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) → ( 𝐼 ‘ 𝑗 ) = 𝑓 )
86 85 adantl ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → ( 𝐼 ‘ 𝑗 ) = 𝑓 )
87 82 86 jca ⊢ ( ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) ∧ ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) ) → ( 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
88 87 ex ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) → ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 ) → ( 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ∧ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) ) )
89 88 reximdv2 ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓 ) → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
90 89 ex ⊢ ( 𝐺 ∈ USHGraph → ( 𝑁 ∈ 𝑓 → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) ) )
91 90 com23 ⊢ ( 𝐺 ∈ USHGraph → ( ∃ 𝑗 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐺 ) ‘ 𝑗 ) = 𝑓 → ( 𝑁 ∈ 𝑓 → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) ) )
92 66 91 sylbid ⊢ ( 𝐺 ∈ USHGraph → ( 𝑓 ∈ ran ( iEdg ‘ 𝐺 ) → ( 𝑁 ∈ 𝑓 → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) ) )
93 51 92 sylbid ⊢ ( 𝐺 ∈ USHGraph → ( 𝑓 ∈ 𝐸 → ( 𝑁 ∈ 𝑓 → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) ) )
94 93 impd ⊢ ( 𝐺 ∈ USHGraph → ( ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
95 94 adantr ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) → ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
96 63 95 impbid ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ↔ ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) ) )
97 vex ⊢ 𝑓 ∈ V
98 eqeq2 ⊢ ( 𝑒 = 𝑓 → ( ( 𝐼 ‘ 𝑗 ) = 𝑒 ↔ ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
99 98 rexbidv ⊢ ( 𝑒 = 𝑓 → ( ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 ↔ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 ) )
100 97 99 elab ⊢ ( 𝑓 ∈ { 𝑒 ∣ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 } ↔ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑓 )
101 eleq2 ⊢ ( 𝑒 = 𝑓 → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑓 ) )
102 101 5 elrab2 ⊢ ( 𝑓 ∈ 𝐵 ↔ ( 𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓 ) )
103 96 100 102 3bitr4g ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑓 ∈ { 𝑒 ∣ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 } ↔ 𝑓 ∈ 𝐵 ) )
104 103 eqrdv ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → { 𝑒 ∣ ∃ 𝑗 ∈ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ( 𝐼 ‘ 𝑗 ) = 𝑒 } = 𝐵 )
105 32 104 eqtrd ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 𝐵 )
106 105 eqcomd ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐵 = ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) )
107 23 13 106 f1oeq123d ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐼 ↾ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) : { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } –1-1-onto→ ( 𝐼 “ { 𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ ( 𝐼 ‘ 𝑖 ) } ) ) )
108 12 107 mpbird ⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )