Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ushgredgedgloop Structured version   Visualization version   GIF version

Theorem ushgredgedgloop 27065
 Description: In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex 𝑁 and the set of loops at this vertex 𝑁. (Contributed by AV, 11-Dec-2020.) (Revised by AV, 6-Jul-2022.)
Hypotheses
Ref Expression
ushgredgedgloop.e 𝐸 = (Edg‘𝐺)
ushgredgedgloop.i 𝐼 = (iEdg‘𝐺)
ushgredgedgloop.a 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}
ushgredgedgloop.b 𝐵 = {𝑒𝐸𝑒 = {𝑁}}
ushgredgedgloop.f 𝐹 = (𝑥𝐴 ↦ (𝐼𝑥))
Assertion
Ref Expression
ushgredgedgloop ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹:𝐴1-1-onto𝐵)
Distinct variable groups:   𝐵,𝑒   𝑒,𝐸,𝑖   𝑒,𝐺,𝑖,𝑥   𝑒,𝐼,𝑖,𝑥   𝑒,𝑁,𝑖,𝑥   𝑒,𝑉,𝑖,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑒,𝑖)   𝐵(𝑥,𝑖)   𝐸(𝑥)   𝐹(𝑥,𝑒,𝑖)

Proof of Theorem ushgredgedgloop
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2798 . . . . 5 (Vtx‘𝐺) = (Vtx‘𝐺)
2 ushgredgedgloop.i . . . . 5 𝐼 = (iEdg‘𝐺)
31, 2ushgrf 26900 . . . 4 (𝐺 ∈ USHGraph → 𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
43adantr 484 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
5 ssrab2 4009 . . 3 {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼
6 f1ores 6613 . . 3 ((𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
74, 5, 6sylancl 589 . 2 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
8 ushgredgedgloop.f . . . . 5 𝐹 = (𝑥𝐴 ↦ (𝐼𝑥))
9 ushgredgedgloop.a . . . . . . 7 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}
109a1i 11 . . . . . 6 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})
11 eqidd 2799 . . . . . 6 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ 𝑥𝐴) → (𝐼𝑥) = (𝐼𝑥))
1210, 11mpteq12dva 5118 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑥𝐴 ↦ (𝐼𝑥)) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
138, 12syl5eq 2845 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹 = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
14 f1f 6557 . . . . . . 7 (𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
153, 14syl 17 . . . . . 6 (𝐺 ∈ USHGraph → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
165a1i 11 . . . . . 6 (𝐺 ∈ USHGraph → {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼)
1715, 16feqresmpt 6719 . . . . 5 (𝐺 ∈ USHGraph → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
1817adantr 484 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
1913, 18eqtr4d 2836 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹 = (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
20 ushgruhgr 26906 . . . . . . . 8 (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph)
21 eqid 2798 . . . . . . . . 9 (iEdg‘𝐺) = (iEdg‘𝐺)
2221uhgrfun 26903 . . . . . . . 8 (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
2320, 22syl 17 . . . . . . 7 (𝐺 ∈ USHGraph → Fun (iEdg‘𝐺))
242funeqi 6353 . . . . . . 7 (Fun 𝐼 ↔ Fun (iEdg‘𝐺))
2523, 24sylibr 237 . . . . . 6 (𝐺 ∈ USHGraph → Fun 𝐼)
2625adantr 484 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → Fun 𝐼)
27 dfimafn 6713 . . . . 5 ((Fun 𝐼 ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒})
2826, 5, 27sylancl 589 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒})
29 fveqeq2 6664 . . . . . . . . . 10 (𝑖 = 𝑗 → ((𝐼𝑖) = {𝑁} ↔ (𝐼𝑗) = {𝑁}))
3029elrab 3630 . . . . . . . . 9 (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↔ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}))
31 simpl 486 . . . . . . . . . . . . . . 15 ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → 𝑗 ∈ dom 𝐼)
32 fvelrn 6831 . . . . . . . . . . . . . . . 16 ((Fun 𝐼𝑗 ∈ dom 𝐼) → (𝐼𝑗) ∈ ran 𝐼)
332eqcomi 2807 . . . . . . . . . . . . . . . . 17 (iEdg‘𝐺) = 𝐼
3433rneqi 5777 . . . . . . . . . . . . . . . 16 ran (iEdg‘𝐺) = ran 𝐼
3532, 34eleqtrrdi 2901 . . . . . . . . . . . . . . 15 ((Fun 𝐼𝑗 ∈ dom 𝐼) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
3626, 31, 35syl2an 598 . . . . . . . . . . . . . 14 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁})) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
37363adant3 1129 . . . . . . . . . . . . 13 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
38 eleq1 2877 . . . . . . . . . . . . . . 15 (𝑓 = (𝐼𝑗) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
3938eqcoms 2806 . . . . . . . . . . . . . 14 ((𝐼𝑗) = 𝑓 → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
40393ad2ant3 1132 . . . . . . . . . . . . 13 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
4137, 40mpbird 260 . . . . . . . . . . . 12 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓 ∈ ran (iEdg‘𝐺))
42 ushgredgedgloop.e . . . . . . . . . . . . . . . 16 𝐸 = (Edg‘𝐺)
43 edgval 26886 . . . . . . . . . . . . . . . . 17 (Edg‘𝐺) = ran (iEdg‘𝐺)
4443a1i 11 . . . . . . . . . . . . . . . 16 (𝐺 ∈ USHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
4542, 44syl5eq 2845 . . . . . . . . . . . . . . 15 (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺))
4645eleq2d 2875 . . . . . . . . . . . . . 14 (𝐺 ∈ USHGraph → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
4746adantr 484 . . . . . . . . . . . . 13 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
48473ad2ant1 1130 . . . . . . . . . . . 12 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
4941, 48mpbird 260 . . . . . . . . . . 11 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓𝐸)
50 eqeq1 2802 . . . . . . . . . . . . . . 15 ((𝐼𝑗) = 𝑓 → ((𝐼𝑗) = {𝑁} ↔ 𝑓 = {𝑁}))
5150biimpcd 252 . . . . . . . . . . . . . 14 ((𝐼𝑗) = {𝑁} → ((𝐼𝑗) = 𝑓𝑓 = {𝑁}))
5251adantl 485 . . . . . . . . . . . . 13 ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓𝑓 = {𝑁}))
5352a1i 11 . . . . . . . . . . . 12 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓𝑓 = {𝑁})))
54533imp 1108 . . . . . . . . . . 11 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓 = {𝑁})
5549, 54jca 515 . . . . . . . . . 10 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓𝐸𝑓 = {𝑁}))
56553exp 1116 . . . . . . . . 9 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁}))))
5730, 56syl5bi 245 . . . . . . . 8 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} → ((𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁}))))
5857rexlimdv 3243 . . . . . . 7 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁})))
5923funfnd 6363 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph → (iEdg‘𝐺) Fn dom (iEdg‘𝐺))
60 fvelrnb 6711 . . . . . . . . . . . 12 ((iEdg‘𝐺) Fn dom (iEdg‘𝐺) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
6159, 60syl 17 . . . . . . . . . . 11 (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
6233dmeqi 5743 . . . . . . . . . . . . . . . . . . . . . 22 dom (iEdg‘𝐺) = dom 𝐼
6362eleq2i 2881 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ dom (iEdg‘𝐺) ↔ 𝑗 ∈ dom 𝐼)
6463biimpi 219 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ dom (iEdg‘𝐺) → 𝑗 ∈ dom 𝐼)
6564adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → 𝑗 ∈ dom 𝐼)
6665adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ dom 𝐼)
6733fveq1i 6656 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((iEdg‘𝐺)‘𝑗) = (𝐼𝑗)
6867eqeq2i 2811 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = ((iEdg‘𝐺)‘𝑗) ↔ 𝑓 = (𝐼𝑗))
6968biimpi 219 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = ((iEdg‘𝐺)‘𝑗) → 𝑓 = (𝐼𝑗))
7069eqcoms 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (((iEdg‘𝐺)‘𝑗) = 𝑓𝑓 = (𝐼𝑗))
7170eqeq1d 2800 . . . . . . . . . . . . . . . . . . . . . 22 (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} ↔ (𝐼𝑗) = {𝑁}))
7271biimpcd 252 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {𝑁} → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = {𝑁}))
7372adantl 485 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = {𝑁}))
7473adantld 494 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼𝑗) = {𝑁}))
7574imp 410 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼𝑗) = {𝑁})
7666, 75jca 515 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}))
7776, 30sylibr 237 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})
7867eqeq1i 2803 . . . . . . . . . . . . . . . . . . 19 (((iEdg‘𝐺)‘𝑗) = 𝑓 ↔ (𝐼𝑗) = 𝑓)
7978biimpi 219 . . . . . . . . . . . . . . . . . 18 (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = 𝑓)
8079adantl 485 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼𝑗) = 𝑓)
8180adantl 485 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼𝑗) = 𝑓)
8277, 81jca 515 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ∧ (𝐼𝑗) = 𝑓))
8382ex 416 . . . . . . . . . . . . . 14 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ∧ (𝐼𝑗) = 𝑓)))
8483reximdv2 3231 . . . . . . . . . . . . 13 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
8584ex 416 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph → (𝑓 = {𝑁} → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
8685com23 86 . . . . . . . . . . 11 (𝐺 ∈ USHGraph → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
8761, 86sylbid 243 . . . . . . . . . 10 (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
8846, 87sylbid 243 . . . . . . . . 9 (𝐺 ∈ USHGraph → (𝑓𝐸 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
8988impd 414 . . . . . . . 8 (𝐺 ∈ USHGraph → ((𝑓𝐸𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9089adantr 484 . . . . . . 7 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑓𝐸𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9158, 90impbid 215 . . . . . 6 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓 ↔ (𝑓𝐸𝑓 = {𝑁})))
92 vex 3445 . . . . . . 7 𝑓 ∈ V
93 eqeq2 2810 . . . . . . . 8 (𝑒 = 𝑓 → ((𝐼𝑗) = 𝑒 ↔ (𝐼𝑗) = 𝑓))
9493rexbidv 3257 . . . . . . 7 (𝑒 = 𝑓 → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒 ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9592, 94elab 3616 . . . . . 6 (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)
96 eqeq1 2802 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = {𝑁} ↔ 𝑓 = {𝑁}))
97 ushgredgedgloop.b . . . . . . 7 𝐵 = {𝑒𝐸𝑒 = {𝑁}}
9896, 97elrab2 3633 . . . . . 6 (𝑓𝐵 ↔ (𝑓𝐸𝑓 = {𝑁}))
9991, 95, 983bitr4g 317 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} ↔ 𝑓𝐵))
10099eqrdv 2796 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} = 𝐵)
10128, 100eqtr2d 2834 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐵 = (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
10219, 10, 101f1oeq123d 6593 . 2 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐹:𝐴1-1-onto𝐵 ↔ (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})))
1037, 102mpbird 260 1 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹:𝐴1-1-onto𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {cab 2776  ∃wrex 3107  {crab 3110   ∖ cdif 3880   ⊆ wss 3883  ∅c0 4246  𝒫 cpw 4500  {csn 4528   ↦ cmpt 5114  dom cdm 5523  ran crn 5524   ↾ cres 5525   “ cima 5526  Fun wfun 6326   Fn wfn 6327  ⟶wf 6328  –1-1→wf1 6329  –1-1-onto→wf1o 6331  ‘cfv 6332  Vtxcvtx 26833  iEdgciedg 26834  Edgcedg 26884  UHGraphcuhgr 26893  USHGraphcushgr 26894 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299  ax-un 7454 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fun 6334  df-fn 6335  df-f 6336  df-f1 6337  df-fo 6338  df-f1o 6339  df-fv 6340  df-edg 26885  df-uhgr 26895  df-ushgr 26896 This theorem is referenced by:  vtxdushgrfvedg  27324
 Copyright terms: Public domain W3C validator