Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | ushgredgedga.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
3 | 1, 2 | ushgrf 25729 |
. . . 4
⊢ (𝐺 ∈ USHGraph → 𝐼:dom 𝐼–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})) |
4 | 3 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐼:dom 𝐼–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅})) |
5 | | ssrab2 3650 |
. . 3
⊢ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ⊆ dom 𝐼 |
6 | | f1ores 6064 |
. . 3
⊢ ((𝐼:dom 𝐼–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) ∧ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ⊆ dom 𝐼) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}):{𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)})) |
7 | 4, 5, 6 | sylancl 693 |
. 2
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}):{𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)})) |
8 | | ushgredgedga.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥)) |
9 | | ushgredgedga.a |
. . . . . . 7
⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} |
10 | 9 | a1i 11 |
. . . . . 6
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐴 = {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) |
11 | | eqidd 2611 |
. . . . . 6
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → (𝐼‘𝑥) = (𝐼‘𝑥)) |
12 | 10, 11 | mpteq12dva 4662 |
. . . . 5
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥)) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↦ (𝐼‘𝑥))) |
13 | 8, 12 | syl5eq 2656 |
. . . 4
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↦ (𝐼‘𝑥))) |
14 | | f1f 6014 |
. . . . . . . 8
⊢ (𝐼:dom 𝐼–1-1→(𝒫 (Vtx‘𝐺) ∖ {∅}) → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖
{∅})) |
15 | 3, 14 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ USHGraph → 𝐼:dom 𝐼⟶(𝒫 (Vtx‘𝐺) ∖
{∅})) |
16 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝐺 ∈ USHGraph → {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ⊆ dom 𝐼) |
17 | 15, 16 | feqresmpt 6160 |
. . . . . 6
⊢ (𝐺 ∈ USHGraph → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↦ (𝐼‘𝑥))) |
18 | 17 | adantr 480 |
. . . . 5
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↦ (𝐼‘𝑥))) |
19 | 18 | eqcomd 2616 |
. . . 4
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↦ (𝐼‘𝑥)) = (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)})) |
20 | 13, 19 | eqtrd 2644 |
. . 3
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 = (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)})) |
21 | | ushgruhgr 25735 |
. . . . . . . . 9
⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph
) |
22 | | eqid 2610 |
. . . . . . . . . 10
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
23 | 22 | uhgrfun 25732 |
. . . . . . . . 9
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
24 | 21, 23 | syl 17 |
. . . . . . . 8
⊢ (𝐺 ∈ USHGraph → Fun
(iEdg‘𝐺)) |
25 | 2 | funeqi 5824 |
. . . . . . . 8
⊢ (Fun
𝐼 ↔ Fun
(iEdg‘𝐺)) |
26 | 24, 25 | sylibr 223 |
. . . . . . 7
⊢ (𝐺 ∈ USHGraph → Fun
𝐼) |
27 | 26 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → Fun 𝐼) |
28 | | dfimafn 6155 |
. . . . . 6
⊢ ((Fun
𝐼 ∧ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ⊆ dom 𝐼) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒}) |
29 | 27, 5, 28 | sylancl 693 |
. . . . 5
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒}) |
30 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑗 → (𝐼‘𝑖) = (𝐼‘𝑗)) |
31 | 30 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑗 → (𝑁 ∈ (𝐼‘𝑖) ↔ 𝑁 ∈ (𝐼‘𝑗))) |
32 | 31 | elrab 3331 |
. . . . . . . . . 10
⊢ (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ↔ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗))) |
33 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) → 𝑗 ∈ dom 𝐼) |
34 | | fvelrn 6260 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐼 ∧ 𝑗 ∈ dom 𝐼) → (𝐼‘𝑗) ∈ ran 𝐼) |
35 | 2 | eqcomi 2619 |
. . . . . . . . . . . . . . . . . . 19
⊢
(iEdg‘𝐺) =
𝐼 |
36 | 35 | rneqi 5273 |
. . . . . . . . . . . . . . . . . 18
⊢ ran
(iEdg‘𝐺) = ran 𝐼 |
37 | 36 | eleq2i 2680 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐼‘𝑗) ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran 𝐼) |
38 | 34, 37 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐼 ∧ 𝑗 ∈ dom 𝐼) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)) |
39 | 27, 33, 38 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗))) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)) |
40 | 39 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)) |
41 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐼‘𝑗) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))) |
42 | 41 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢ ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))) |
43 | 42 | 3ad2ant3 1077 |
. . . . . . . . . . . . . 14
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))) |
44 | 40, 43 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → 𝑓 ∈ ran (iEdg‘𝐺)) |
45 | | ushgredgedga.e |
. . . . . . . . . . . . . . . . 17
⊢ 𝐸 = (Edg‘𝐺) |
46 | | edgaval 25794 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ USHGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
47 | 45, 46 | syl5eq 2656 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺)) |
48 | 47 | eleq2d 2673 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺))) |
49 | 48 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺))) |
50 | 49 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺))) |
51 | 44, 50 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → 𝑓 ∈ 𝐸) |
52 | | eleq2 2677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐼‘𝑗) = 𝑓 → (𝑁 ∈ (𝐼‘𝑗) ↔ 𝑁 ∈ 𝑓)) |
53 | 52 | biimpcd 238 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ (𝐼‘𝑗) → ((𝐼‘𝑗) = 𝑓 → 𝑁 ∈ 𝑓)) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) → ((𝐼‘𝑗) = 𝑓 → 𝑁 ∈ 𝑓)) |
55 | 54 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) → ((𝐼‘𝑗) = 𝑓 → 𝑁 ∈ 𝑓))) |
56 | 55 | 3imp 1249 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → 𝑁 ∈ 𝑓) |
57 | 51, 56 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓)) |
58 | 57 | 3exp 1256 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗)) → ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓)))) |
59 | 32, 58 | syl5bi 231 |
. . . . . . . . 9
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} → ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓)))) |
60 | 59 | rexlimdv 3012 |
. . . . . . . 8
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓))) |
61 | | funfn 5833 |
. . . . . . . . . . . . . . 15
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
62 | 61 | biimpi 205 |
. . . . . . . . . . . . . 14
⊢ (Fun
(iEdg‘𝐺) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
63 | 24, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USHGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
64 | | fvelrnb 6153 |
. . . . . . . . . . . . 13
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
(𝑓 ∈ ran
(iEdg‘𝐺) ↔
∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓)) |
66 | 35 | dmeqi 5247 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ dom
(iEdg‘𝐺) = dom 𝐼 |
67 | 66 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 ∈ dom (iEdg‘𝐺) ↔ 𝑗 ∈ dom 𝐼) |
68 | 67 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑗 ∈ dom (iEdg‘𝐺) → 𝑗 ∈ dom 𝐼) |
69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → 𝑗 ∈ dom 𝐼) |
70 | 69 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ dom 𝐼) |
71 | 35 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((iEdg‘𝐺)‘𝑗) = (𝐼‘𝑗) |
72 | 71 | eqeq2i 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = ((iEdg‘𝐺)‘𝑗) ↔ 𝑓 = (𝐼‘𝑗)) |
73 | 72 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = ((iEdg‘𝐺)‘𝑗) → 𝑓 = (𝐼‘𝑗)) |
74 | 73 | eqcoms 2618 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((iEdg‘𝐺)‘𝑗) = 𝑓 → 𝑓 = (𝐼‘𝑗)) |
75 | 74 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑁 ∈ 𝑓 ↔ 𝑁 ∈ (𝐼‘𝑗))) |
76 | 75 | biimpcd 238 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ 𝑓 → (((iEdg‘𝐺)‘𝑗) = 𝑓 → 𝑁 ∈ (𝐼‘𝑗))) |
77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) → (((iEdg‘𝐺)‘𝑗) = 𝑓 → 𝑁 ∈ (𝐼‘𝑗))) |
78 | 77 | adantld 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → 𝑁 ∈ (𝐼‘𝑗))) |
79 | 78 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑁 ∈ (𝐼‘𝑗)) |
80 | 70, 79 | jca 553 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ dom 𝐼 ∧ 𝑁 ∈ (𝐼‘𝑗))) |
81 | 80, 32 | sylibr 223 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) |
82 | 71 | eqeq1i 2615 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((iEdg‘𝐺)‘𝑗) = 𝑓 ↔ (𝐼‘𝑗) = 𝑓) |
83 | 82 | biimpi 205 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼‘𝑗) = 𝑓) |
84 | 83 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼‘𝑗) = 𝑓) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼‘𝑗) = 𝑓) |
86 | 81, 85 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ∧ (𝐼‘𝑗) = 𝑓)) |
87 | 86 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} ∧ (𝐼‘𝑗) = 𝑓))) |
88 | 87 | reximdv2 2997 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑓) → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓)) |
89 | 88 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USHGraph → (𝑁 ∈ 𝑓 → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓))) |
90 | 89 | com23 84 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ USHGraph →
(∃𝑗 ∈ dom
(iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑁 ∈ 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓))) |
91 | 65, 90 | sylbid 229 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) → (𝑁 ∈ 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓))) |
92 | 48, 91 | sylbid 229 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ 𝐸 → (𝑁 ∈ 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓))) |
93 | 92 | impd 446 |
. . . . . . . . 9
⊢ (𝐺 ∈ USHGraph → ((𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓)) |
94 | 93 | adantr 480 |
. . . . . . . 8
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓)) |
95 | 60, 94 | impbid 201 |
. . . . . . 7
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓 ↔ (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓))) |
96 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
97 | | eqeq2 2621 |
. . . . . . . . 9
⊢ (𝑒 = 𝑓 → ((𝐼‘𝑗) = 𝑒 ↔ (𝐼‘𝑗) = 𝑓)) |
98 | 97 | rexbidv 3034 |
. . . . . . . 8
⊢ (𝑒 = 𝑓 → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒 ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓)) |
99 | 96, 98 | elab 3319 |
. . . . . . 7
⊢ (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒} ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑓) |
100 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑒 = 𝑓 → (𝑁 ∈ 𝑒 ↔ 𝑁 ∈ 𝑓)) |
101 | | ushgredgedga.b |
. . . . . . . 8
⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒} |
102 | 100, 101 | elrab2 3333 |
. . . . . . 7
⊢ (𝑓 ∈ 𝐵 ↔ (𝑓 ∈ 𝐸 ∧ 𝑁 ∈ 𝑓)) |
103 | 95, 99, 102 | 3bitr4g 302 |
. . . . . 6
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒} ↔ 𝑓 ∈ 𝐵)) |
104 | 103 | eqrdv 2608 |
. . . . 5
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)} (𝐼‘𝑗) = 𝑒} = 𝐵) |
105 | 29, 104 | eqtrd 2644 |
. . . 4
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}) = 𝐵) |
106 | 105 | eqcomd 2616 |
. . 3
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐵 = (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)})) |
107 | 20, 10, 106 | f1oeq123d 6046 |
. 2
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}):{𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ 𝑁 ∈ (𝐼‘𝑖)}))) |
108 | 7, 107 | mpbird 246 |
1
⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵) |