Step | Hyp | Ref
| Expression |
1 | | usgruspgr 26073 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph
) |
2 | | edgusgr 26055 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝑒) = 2)) |
3 | 2 | simprd 479 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (#‘𝑒) = 2) |
4 | 3 | ralrimiva 2966 |
. . 3
⊢ (𝐺 ∈ USGraph →
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) |
5 | 1, 4 | jca 554 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2)) |
6 | | edgval 25941 |
. . . . . . 7
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
8 | 7 | raleqdv 3144 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2 ↔ ∀𝑒 ∈ ran (iEdg‘𝐺)(#‘𝑒) = 2)) |
9 | | eqid 2622 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
10 | | eqid 2622 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
11 | 9, 10 | uspgrf 26049 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
12 | | f1f 6101 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
13 | | frn 6053 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
15 | | ssel2 3598 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2} ∧ 𝑦 ∈ ran (iEdg‘𝐺)) → 𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
16 | 15 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
𝑦 ∈ {𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (#‘𝑥) ≤ 2})) |
17 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑦 → (#‘𝑒) = (#‘𝑦)) |
18 | 17 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑦 → ((#‘𝑒) = 2 ↔ (#‘𝑦) = 2)) |
19 | 18 | rspcv 3305 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (∀𝑒 ∈ ran (iEdg‘𝐺)(#‘𝑒) = 2 → (#‘𝑦) = 2)) |
20 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (#‘𝑥) = (#‘𝑦)) |
21 | 20 | breq1d 4663 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((#‘𝑥) ≤ 2 ↔ (#‘𝑦) ≤ 2)) |
22 | 21 | elrab 3363 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ↔
(𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) ≤ 2)) |
23 | | eldifi 3732 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → 𝑦 ∈
𝒫 (Vtx‘𝐺)) |
24 | 23 | anim1i 592 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) = 2) → (𝑦 ∈ 𝒫 (Vtx‘𝐺) ∧ (#‘𝑦) = 2)) |
25 | 20 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((#‘𝑥) = 2 ↔ (#‘𝑦) = 2)) |
26 | 25 | elrab 3363 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2} ↔ (𝑦 ∈ 𝒫
(Vtx‘𝐺) ∧
(#‘𝑦) =
2)) |
27 | 24, 26 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) = 2) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
28 | 27 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → ((#‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
29 | 28 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (#‘𝑦) ≤ 2) → ((#‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
30 | 22, 29 | sylbi 207 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
((#‘𝑦) = 2 →
𝑦 ∈ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2})) |
31 | 19, 30 | syl9 77 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
32 | 16, 31 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
33 | 32 | com13 88 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}))) |
34 | 33 | imp 445 |
. . . . . . . . . . 11
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2}) →
(𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
35 | 34 | ssrdv 3609 |
. . . . . . . . . 10
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2}) →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2}) |
36 | 35 | ex 450 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(#‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) =
2})) |
37 | 14, 36 | mpan9 486 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2) → ran (iEdg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
38 | | f1ssr 6107 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
ran (iEdg‘𝐺) ⊆
{𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(#‘𝑥) = 2}) →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
39 | 37, 38 | syldan 487 |
. . . . . . 7
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∧
∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
40 | 39 | ex 450 |
. . . . . 6
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
41 | 11, 40 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
42 | 8, 41 | sylbid 230 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
43 | 42 | imp 445 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2}) |
44 | 9, 10 | isusgrs 26051 |
. . . 4
⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
45 | 44 | adantr 481 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑥) = 2})) |
46 | 43, 45 | mpbird 247 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2) → 𝐺 ∈ USGraph ) |
47 | 5, 46 | impbii 199 |
1
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(#‘𝑒) = 2)) |