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

Theorem ushgredgedgloopOLD 26535
 Description: Obsolete version of ushgredgedgloop 26534 as of 6-Jul-2022. (Contributed by AV, 11-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
ushgredgedgloopOLD.e 𝐸 = (Edg‘𝐺)
ushgredgedgloopOLD.i 𝐼 = (iEdg‘𝐺)
ushgredgedgloopOLD.v 𝑉 = (Vtx‘𝐺)
ushgredgedgloopOLD.a 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}
ushgredgedgloopOLD.b 𝐵 = {𝑒𝐸𝑒 = {𝑁}}
ushgredgedgloopOLD.f 𝐹 = (𝑥𝐴 ↦ (𝐼𝑥))
Assertion
Ref Expression
ushgredgedgloopOLD ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹:𝐴1-1-onto𝐵)
Distinct variable groups:   𝐵,𝑒   𝑒,𝐸,𝑖   𝑒,𝐺,𝑖,𝑥   𝑒,𝐼,𝑖,𝑥   𝑒,𝑁,𝑖,𝑥   𝑒,𝑉,𝑖,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑒,𝑖)   𝐵(𝑥,𝑖)   𝐸(𝑥)   𝐹(𝑥,𝑒,𝑖)

Proof of Theorem ushgredgedgloopOLD
Dummy variables 𝑓 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2825 . . . . 5 (Vtx‘𝐺) = (Vtx‘𝐺)
2 ushgredgedgloopOLD.i . . . . 5 𝐼 = (iEdg‘𝐺)
31, 2ushgrf 26368 . . . 4 (𝐺 ∈ USHGraph → 𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
43adantr 474 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}))
5 ssrab2 3914 . . 3 {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼
6 f1ores 6396 . . 3 ((𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
74, 5, 6sylancl 580 . 2 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
8 ushgredgedgloopOLD.f . . . . 5 𝐹 = (𝑥𝐴 ↦ (𝐼𝑥))
9 ushgredgedgloopOLD.a . . . . . . 7 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}
109a1i 11 . . . . . 6 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})
11 eqidd 2826 . . . . . 6 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ 𝑥𝐴) → (𝐼𝑥) = (𝐼𝑥))
1210, 11mpteq12dva 4957 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑥𝐴 ↦ (𝐼𝑥)) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
138, 12syl5eq 2873 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹 = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
14 f1f 6342 . . . . . . 7 (𝐼:dom 𝐼1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
153, 14syl 17 . . . . . 6 (𝐺 ∈ USHGraph → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖ {∅}))
165a1i 11 . . . . . 6 (𝐺 ∈ USHGraph → {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼)
1715, 16feqresmpt 6501 . . . . 5 (𝐺 ∈ USHGraph → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
1817adantr 474 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↦ (𝐼𝑥)))
1913, 18eqtr4d 2864 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹 = (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
20 ushgruhgr 26374 . . . . . . . 8 (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph)
21 eqid 2825 . . . . . . . . 9 (iEdg‘𝐺) = (iEdg‘𝐺)
2221uhgrfun 26371 . . . . . . . 8 (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
2320, 22syl 17 . . . . . . 7 (𝐺 ∈ USHGraph → Fun (iEdg‘𝐺))
242funeqi 6148 . . . . . . 7 (Fun 𝐼 ↔ Fun (iEdg‘𝐺))
2523, 24sylibr 226 . . . . . 6 (𝐺 ∈ USHGraph → Fun 𝐼)
2625adantr 474 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → Fun 𝐼)
27 dfimafn 6496 . . . . 5 ((Fun 𝐼 ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒})
2826, 5, 27sylancl 580 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒})
29 fveq2 6437 . . . . . . . . . . 11 (𝑖 = 𝑗 → (𝐼𝑖) = (𝐼𝑗))
3029eqeq1d 2827 . . . . . . . . . 10 (𝑖 = 𝑗 → ((𝐼𝑖) = {𝑁} ↔ (𝐼𝑗) = {𝑁}))
3130elrab 3585 . . . . . . . . 9 (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ↔ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}))
32 simpl 476 . . . . . . . . . . . . . . 15 ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → 𝑗 ∈ dom 𝐼)
33 fvelrn 6606 . . . . . . . . . . . . . . . 16 ((Fun 𝐼𝑗 ∈ dom 𝐼) → (𝐼𝑗) ∈ ran 𝐼)
342eqcomi 2834 . . . . . . . . . . . . . . . . 17 (iEdg‘𝐺) = 𝐼
3534rneqi 5588 . . . . . . . . . . . . . . . 16 ran (iEdg‘𝐺) = ran 𝐼
3633, 35syl6eleqr 2917 . . . . . . . . . . . . . . 15 ((Fun 𝐼𝑗 ∈ dom 𝐼) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
3726, 32, 36syl2an 589 . . . . . . . . . . . . . 14 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁})) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
38373adant3 1166 . . . . . . . . . . . . 13 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝐼𝑗) ∈ ran (iEdg‘𝐺))
39 eleq1 2894 . . . . . . . . . . . . . . 15 (𝑓 = (𝐼𝑗) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
4039eqcoms 2833 . . . . . . . . . . . . . 14 ((𝐼𝑗) = 𝑓 → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
41403ad2ant3 1169 . . . . . . . . . . . . 13 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼𝑗) ∈ ran (iEdg‘𝐺)))
4238, 41mpbird 249 . . . . . . . . . . . 12 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓 ∈ ran (iEdg‘𝐺))
43 ushgredgedgloopOLD.e . . . . . . . . . . . . . . . 16 𝐸 = (Edg‘𝐺)
44 edgval 26354 . . . . . . . . . . . . . . . . 17 (Edg‘𝐺) = ran (iEdg‘𝐺)
4544a1i 11 . . . . . . . . . . . . . . . 16 (𝐺 ∈ USHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
4643, 45syl5eq 2873 . . . . . . . . . . . . . . 15 (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺))
4746eleq2d 2892 . . . . . . . . . . . . . 14 (𝐺 ∈ USHGraph → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
4847adantr 474 . . . . . . . . . . . . 13 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
49483ad2ant1 1167 . . . . . . . . . . . 12 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓𝐸𝑓 ∈ ran (iEdg‘𝐺)))
5042, 49mpbird 249 . . . . . . . . . . 11 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓𝐸)
51 eqeq1 2829 . . . . . . . . . . . . . . 15 ((𝐼𝑗) = 𝑓 → ((𝐼𝑗) = {𝑁} ↔ 𝑓 = {𝑁}))
5251biimpcd 241 . . . . . . . . . . . . . 14 ((𝐼𝑗) = {𝑁} → ((𝐼𝑗) = 𝑓𝑓 = {𝑁}))
5352adantl 475 . . . . . . . . . . . . 13 ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓𝑓 = {𝑁}))
5453a1i 11 . . . . . . . . . . . 12 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓𝑓 = {𝑁})))
55543imp 1141 . . . . . . . . . . 11 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → 𝑓 = {𝑁})
5650, 55jca 507 . . . . . . . . . 10 (((𝐺 ∈ USHGraph ∧ 𝑁𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) ∧ (𝐼𝑗) = 𝑓) → (𝑓𝐸𝑓 = {𝑁}))
57563exp 1152 . . . . . . . . 9 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}) → ((𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁}))))
5831, 57syl5bi 234 . . . . . . . 8 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} → ((𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁}))))
5958rexlimdv 3239 . . . . . . 7 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓 → (𝑓𝐸𝑓 = {𝑁})))
60 funfn 6157 . . . . . . . . . . . . . 14 (Fun (iEdg‘𝐺) ↔ (iEdg‘𝐺) Fn dom (iEdg‘𝐺))
6160biimpi 208 . . . . . . . . . . . . 13 (Fun (iEdg‘𝐺) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺))
6223, 61syl 17 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph → (iEdg‘𝐺) Fn dom (iEdg‘𝐺))
63 fvelrnb 6494 . . . . . . . . . . . 12 ((iEdg‘𝐺) Fn dom (iEdg‘𝐺) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
6462, 63syl 17 . . . . . . . . . . 11 (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
6534dmeqi 5561 . . . . . . . . . . . . . . . . . . . . . 22 dom (iEdg‘𝐺) = dom 𝐼
6665eleq2i 2898 . . . . . . . . . . . . . . . . . . . . 21 (𝑗 ∈ dom (iEdg‘𝐺) ↔ 𝑗 ∈ dom 𝐼)
6766biimpi 208 . . . . . . . . . . . . . . . . . . . 20 (𝑗 ∈ dom (iEdg‘𝐺) → 𝑗 ∈ dom 𝐼)
6867adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → 𝑗 ∈ dom 𝐼)
6968adantl 475 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ dom 𝐼)
7034fveq1i 6438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((iEdg‘𝐺)‘𝑗) = (𝐼𝑗)
7170eqeq2i 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑓 = ((iEdg‘𝐺)‘𝑗) ↔ 𝑓 = (𝐼𝑗))
7271biimpi 208 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = ((iEdg‘𝐺)‘𝑗) → 𝑓 = (𝐼𝑗))
7372eqcoms 2833 . . . . . . . . . . . . . . . . . . . . . . 23 (((iEdg‘𝐺)‘𝑗) = 𝑓𝑓 = (𝐼𝑗))
7473eqeq1d 2827 . . . . . . . . . . . . . . . . . . . . . 22 (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} ↔ (𝐼𝑗) = {𝑁}))
7574biimpcd 241 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = {𝑁} → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = {𝑁}))
7675adantl 475 . . . . . . . . . . . . . . . . . . . 20 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = {𝑁}))
7776adantld 486 . . . . . . . . . . . . . . . . . . 19 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼𝑗) = {𝑁}))
7877imp 397 . . . . . . . . . . . . . . . . . 18 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼𝑗) = {𝑁})
7969, 78jca 507 . . . . . . . . . . . . . . . . 17 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ dom 𝐼 ∧ (𝐼𝑗) = {𝑁}))
8079, 31sylibr 226 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})
8170eqeq1i 2830 . . . . . . . . . . . . . . . . . . 19 (((iEdg‘𝐺)‘𝑗) = 𝑓 ↔ (𝐼𝑗) = 𝑓)
8281biimpi 208 . . . . . . . . . . . . . . . . . 18 (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼𝑗) = 𝑓)
8382adantl 475 . . . . . . . . . . . . . . . . 17 ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼𝑗) = 𝑓)
8483adantl 475 . . . . . . . . . . . . . . . 16 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼𝑗) = 𝑓)
8580, 84jca 507 . . . . . . . . . . . . . . 15 (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ∧ (𝐼𝑗) = 𝑓))
8685ex 403 . . . . . . . . . . . . . 14 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} ∧ (𝐼𝑗) = 𝑓)))
8786reximdv2 3222 . . . . . . . . . . . . 13 ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
8887ex 403 . . . . . . . . . . . 12 (𝐺 ∈ USHGraph → (𝑓 = {𝑁} → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
8988com23 86 . . . . . . . . . . 11 (𝐺 ∈ USHGraph → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
9064, 89sylbid 232 . . . . . . . . . 10 (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
9147, 90sylbid 232 . . . . . . . . 9 (𝐺 ∈ USHGraph → (𝑓𝐸 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)))
9291impd 400 . . . . . . . 8 (𝐺 ∈ USHGraph → ((𝑓𝐸𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9392adantr 474 . . . . . . 7 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → ((𝑓𝐸𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9459, 93impbid 204 . . . . . 6 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓 ↔ (𝑓𝐸𝑓 = {𝑁})))
95 vex 3417 . . . . . . 7 𝑓 ∈ V
96 eqeq2 2836 . . . . . . . 8 (𝑒 = 𝑓 → ((𝐼𝑗) = 𝑒 ↔ (𝐼𝑗) = 𝑓))
9796rexbidv 3262 . . . . . . 7 (𝑒 = 𝑓 → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒 ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓))
9895, 97elab 3571 . . . . . 6 (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑓)
99 eqeq1 2829 . . . . . . 7 (𝑒 = 𝑓 → (𝑒 = {𝑁} ↔ 𝑓 = {𝑁}))
100 ushgredgedgloopOLD.b . . . . . . 7 𝐵 = {𝑒𝐸𝑒 = {𝑁}}
10199, 100elrab2 3589 . . . . . 6 (𝑓𝐵 ↔ (𝑓𝐸𝑓 = {𝑁}))
10294, 98, 1013bitr4g 306 . . . . 5 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} ↔ 𝑓𝐵))
103102eqrdv 2823 . . . 4 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}} (𝐼𝑗) = 𝑒} = 𝐵)
10428, 103eqtr2d 2862 . . 3 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐵 = (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}))
10519, 10, 104f1oeq123d 6377 . 2 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → (𝐹:𝐴1-1-onto𝐵 ↔ (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼𝑖) = {𝑁}})))
1067, 105mpbird 249 1 ((𝐺 ∈ USHGraph ∧ 𝑁𝑉) → 𝐹:𝐴1-1-onto𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1111   = wceq 1656   ∈ wcel 2164  {cab 2811  ∃wrex 3118  {crab 3121   ∖ cdif 3795   ⊆ wss 3798  ∅c0 4146  𝒫 cpw 4380  {csn 4399   ↦ cmpt 4954  dom cdm 5346  ran crn 5347   ↾ cres 5348   “ cima 5349  Fun wfun 6121   Fn wfn 6122  ⟶wf 6123  –1-1→wf1 6124  –1-1-onto→wf1o 6126  ‘cfv 6127  Vtxcvtx 26301  iEdgciedg 26302  Edgcedg 26352  UHGraphcuhgr 26361  USHGraphcushgr 26362 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-edg 26353  df-uhgr 26363  df-ushgr 26364 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator