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

Proof

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