| Step | Hyp | Ref
| Expression |
| 1 | | df-ima 5698 |
. 2
⊢ (𝐸 “ 𝐹) = ran (𝐸 ↾ 𝐹) |
| 2 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑗 → (𝐸‘𝑖) = (𝐸‘𝑗)) |
| 3 | | neleq2 3053 |
. . . . . . 7
⊢ ((𝐸‘𝑖) = (𝐸‘𝑗) → (𝑁 ∉ (𝐸‘𝑖) ↔ 𝑁 ∉ (𝐸‘𝑗))) |
| 4 | 2, 3 | syl 17 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑁 ∉ (𝐸‘𝑖) ↔ 𝑁 ∉ (𝐸‘𝑗))) |
| 5 | | upgrres.f |
. . . . . 6
⊢ 𝐹 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)} |
| 6 | 4, 5 | elrab2 3695 |
. . . . 5
⊢ (𝑗 ∈ 𝐹 ↔ (𝑗 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑗))) |
| 7 | | upgrres.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
| 8 | | upgrres.e |
. . . . . . . 8
⊢ 𝐸 = (iEdg‘𝐺) |
| 9 | 7, 8 | upgrf 29103 |
. . . . . . 7
⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
| 10 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝐸:dom 𝐸⟶{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
∧ 𝑗 ∈ dom 𝐸) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
| 11 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑝 = (𝐸‘𝑗) → (♯‘𝑝) = (♯‘(𝐸‘𝑗))) |
| 12 | 11 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ (𝑝 = (𝐸‘𝑗) → ((♯‘𝑝) ≤ 2 ↔ (♯‘(𝐸‘𝑗)) ≤ 2)) |
| 13 | 12 | elrab 3692 |
. . . . . . . . . . 11
⊢ ((𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
↔ ((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2)) |
| 14 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ↔ ((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ (𝐸‘𝑗) ≠ ∅)) |
| 15 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ 𝒫 𝑉) |
| 16 | | elpwi 4607 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸‘𝑗) ∈ 𝒫 𝑉 → (𝐸‘𝑗) ⊆ 𝑉) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ⊆ 𝑉) |
| 18 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ (𝐸‘𝑗)) → 𝑁 ∉ (𝐸‘𝑗)) |
| 19 | | elpwdifsn 4789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ (𝐸‘𝑗) ⊆ 𝑉 ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
| 20 | 15, 17, 18, 19 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
| 21 | 20 | ex 412 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐸‘𝑗) ∈ 𝒫 𝑉 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 22 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐸‘𝑗) ∈ 𝒫 𝑉 ∧ (𝐸‘𝑗) ≠ ∅) → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 23 | 14, 22 | sylbi 217 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 24 | 23 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}))) |
| 25 | 24 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁})) |
| 26 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) → (𝐸‘𝑗) ≠ ∅) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) → (𝐸‘𝑗) ≠ ∅) |
| 28 | 27 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ≠ ∅) |
| 29 | | eldifsn 4786 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸‘𝑗) ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ↔ ((𝐸‘𝑗) ∈ 𝒫 (𝑉 ∖ {𝑁}) ∧ (𝐸‘𝑗) ≠ ∅)) |
| 30 | 25, 28, 29 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅})) |
| 31 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) → (♯‘(𝐸‘𝑗)) ≤ 2) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) ∧ 𝑁 ∉ (𝐸‘𝑗)) → (♯‘(𝐸‘𝑗)) ≤ 2) |
| 33 | 12, 30, 32 | elrabd 3694 |
. . . . . . . . . . . . 13
⊢ ((((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
| 34 | 33 | ex 412 |
. . . . . . . . . . . 12
⊢ (((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
| 35 | 34 | a1d 25 |
. . . . . . . . . . 11
⊢ (((𝐸‘𝑗) ∈ (𝒫 𝑉 ∖ {∅}) ∧
(♯‘(𝐸‘𝑗)) ≤ 2) → (𝑁 ∈ 𝑉 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}))) |
| 36 | 13, 35 | sylbi 217 |
. . . . . . . . . 10
⊢ ((𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
→ (𝑁 ∈ 𝑉 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}))) |
| 37 | 10, 36 | syl 17 |
. . . . . . . . 9
⊢ ((𝐸:dom 𝐸⟶{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
∧ 𝑗 ∈ dom 𝐸) → (𝑁 ∈ 𝑉 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}))) |
| 38 | 37 | ex 412 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸⟶{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
→ (𝑗 ∈ dom 𝐸 → (𝑁 ∈ 𝑉 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})))) |
| 39 | 38 | com23 86 |
. . . . . . 7
⊢ (𝐸:dom 𝐸⟶{𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
→ (𝑁 ∈ 𝑉 → (𝑗 ∈ dom 𝐸 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})))) |
| 40 | 9, 39 | syl 17 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → (𝑁 ∈ 𝑉 → (𝑗 ∈ dom 𝐸 → (𝑁 ∉ (𝐸‘𝑗) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})))) |
| 41 | 40 | imp4b 421 |
. . . . 5
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐸 ∧ 𝑁 ∉ (𝐸‘𝑗)) → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
| 42 | 6, 41 | biimtrid 242 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝑗 ∈ 𝐹 → (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
| 43 | 42 | ralrimiv 3145 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ∀𝑗 ∈ 𝐹 (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
| 44 | | upgruhgr 29119 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
| 45 | 8 | uhgrfun 29083 |
. . . . . 6
⊢ (𝐺 ∈ UHGraph → Fun 𝐸) |
| 46 | 44, 45 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → Fun 𝐸) |
| 47 | 46 | adantr 480 |
. . . 4
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → Fun 𝐸) |
| 48 | 5 | ssrab3 4082 |
. . . 4
⊢ 𝐹 ⊆ dom 𝐸 |
| 49 | | funimass4 6973 |
. . . 4
⊢ ((Fun
𝐸 ∧ 𝐹 ⊆ dom 𝐸) → ((𝐸 “ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
↔ ∀𝑗 ∈
𝐹 (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
| 50 | 47, 48, 49 | sylancl 586 |
. . 3
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ((𝐸 “ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
↔ ∀𝑗 ∈
𝐹 (𝐸‘𝑗) ∈ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
| 51 | 43, 50 | mpbird 257 |
. 2
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → (𝐸 “ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
| 52 | 1, 51 | eqsstrrid 4023 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) → ran (𝐸 ↾ 𝐹) ⊆ {𝑝 ∈ (𝒫 (𝑉 ∖ {𝑁}) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |