Step | Hyp | Ref
| Expression |
1 | | edgval 25941 |
. . . . 5
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝐺 ∈ UPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
3 | 2 | eleq2d 2687 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝐸 ∈ (Edg‘𝐺) ↔ 𝐸 ∈ ran (iEdg‘𝐺))) |
4 | | eqid 2622 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
5 | | eqid 2622 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
6 | 4, 5 | upgrf 25981 |
. . . . . 6
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
7 | | frn 6053 |
. . . . . 6
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
9 | 8 | sseld 3602 |
. . . 4
⊢ (𝐺 ∈ UPGraph → (𝐸 ∈ ran (iEdg‘𝐺) → 𝐸 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2})) |
10 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = 𝐸 → (#‘𝑥) = (#‘𝐸)) |
11 | 10 | breq1d 4663 |
. . . . . 6
⊢ (𝑥 = 𝐸 → ((#‘𝑥) ≤ 2 ↔ (#‘𝐸) ≤ 2)) |
12 | 11 | elrab 3363 |
. . . . 5
⊢ (𝐸 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ↔
(𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝐸) ≤ 2)) |
13 | | eldifsn 4317 |
. . . . . . . . 9
⊢ (𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ↔ (𝐸 ∈
𝒫 (Vtx‘𝐺)
∧ 𝐸 ≠
∅)) |
14 | 13 | biimpi 206 |
. . . . . . . 8
⊢ (𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → (𝐸 ∈
𝒫 (Vtx‘𝐺)
∧ 𝐸 ≠
∅)) |
15 | 14 | anim1i 592 |
. . . . . . 7
⊢ ((𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝐸) ≤ 2) → ((𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅) ∧ (#‘𝐸) ≤ 2)) |
16 | | df-3an 1039 |
. . . . . . 7
⊢ ((𝐸 ∈ 𝒫
(Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧
(#‘𝐸) ≤ 2) ↔
((𝐸 ∈ 𝒫
(Vtx‘𝐺) ∧ 𝐸 ≠ ∅) ∧
(#‘𝐸) ≤
2)) |
17 | 15, 16 | sylibr 224 |
. . . . . 6
⊢ ((𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝐸) ≤ 2) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2)) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → ((𝐸 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝐸) ≤ 2) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2))) |
19 | 12, 18 | syl5bi 232 |
. . . 4
⊢ (𝐺 ∈ UPGraph → (𝐸 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(𝐸 ∈ 𝒫
(Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧
(#‘𝐸) ≤
2))) |
20 | 9, 19 | syld 47 |
. . 3
⊢ (𝐺 ∈ UPGraph → (𝐸 ∈ ran (iEdg‘𝐺) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2))) |
21 | 3, 20 | sylbid 230 |
. 2
⊢ (𝐺 ∈ UPGraph → (𝐸 ∈ (Edg‘𝐺) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2))) |
22 | 21 | imp 445 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝐸 ∈ (Edg‘𝐺)) → (𝐸 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝐸 ≠ ∅ ∧ (#‘𝐸) ≤ 2)) |