Step | Hyp | Ref
| Expression |
1 | | usgruspgr 40408 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph
) |
2 | | edgusgr 40391 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝑒) = 2)) |
3 | 2 | simprd 478 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (#‘𝑒) = 2) |
4 | 3 | ralrimiva 2949 |
. . 3
⊢ (𝐺 ∈ USGraph →
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) |
5 | 1, 4 | jca 553 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2)) |
6 | | edgaval 25794 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
7 | 6 | raleqdv 3121 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2 ↔ ∀𝑒 ∈ ran (iEdg‘𝐺)(#‘𝑒) = 2)) |
8 | | eqid 2610 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
9 | | eqid 2610 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
10 | 8, 9 | uspgrf 40384 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
11 | | f1f 6014 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
12 | | frn 5966 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
14 | | ssel2 3563 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2} ∧ 𝑦 ∈ ran (iEdg‘𝐺)) → 𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
15 | 14 | expcom 450 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
𝑦 ∈ {𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2})) |
16 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑦 → (#‘𝑒) = (#‘𝑦)) |
17 | 16 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑦 → ((#‘𝑒) = 2 ↔ (#‘𝑦) = 2)) |
18 | 17 | rspcv 3278 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (∀𝑒 ∈ ran (iEdg‘𝐺)(#‘𝑒) = 2 → (#‘𝑦) = 2)) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
20 | 19 | breq1d 4593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((#‘𝑥) ≤ 2 ↔ (#‘𝑦) ≤ 2)) |
21 | 20 | elrab 3331 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ↔
(𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) ≤ 2)) |
22 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → 𝑦 ∈
𝒫 (Vtx‘𝐺)) |
23 | 22 | anim1i 590 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) = 2) → (𝑦 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝑦) = 2)) |
24 | 19 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = 2 ↔ (#‘𝑦) = 2)) |
25 | 24 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2} ↔ (𝑦 ∈ 𝒫
(Vtx‘𝐺) ∧
(#‘𝑦) =
2)) |
26 | 23, 25 | sylibr 223 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) = 2) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
27 | 26 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → ((#‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) ≤ 2) → ((#‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
29 | 21, 28 | sylbi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
((#‘𝑦) = 2 →
𝑦 ∈ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2})) |
30 | 18, 29 | syl9 75 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
31 | 15, 30 | syld 46 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
32 | 31 | com13 86 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
33 | 32 | imp 444 |
. . . . . . . . . . 11
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2}) →
(𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
34 | 33 | ssrdv 3574 |
. . . . . . . . . 10
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2}) →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2}) |
35 | 34 | ex 449 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2})) |
36 | 13, 35 | mpan9 485 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2) → ran (iEdg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
37 | | f1ssr 6020 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) = 2}) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
38 | 36, 37 | syldan 486 |
. . . . . . 7
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
39 | 38 | ex 449 |
. . . . . 6
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
40 | 10, 39 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
41 | 7, 40 | sylbid 229 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
42 | 41 | imp 444 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
43 | 8, 9 | isusgrs 40386 |
. . . 4
⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
44 | 43 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
45 | 42, 44 | mpbird 246 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → 𝐺 ∈ USGraph ) |
46 | 5, 45 | impbii 198 |
1
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2)) |