Step | Hyp | Ref
| Expression |
1 | | usgruspgr 27293 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
2 | | edgusgr 27275 |
. . . . 5
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝑒) = 2)) |
3 | 2 | simprd 499 |
. . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (♯‘𝑒) = 2) |
4 | 3 | ralrimiva 3106 |
. . 3
⊢ (𝐺 ∈ USGraph →
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) |
5 | 1, 4 | jca 515 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2)) |
6 | | edgval 27164 |
. . . . . . 7
⊢
(Edg‘𝐺) = ran
(iEdg‘𝐺) |
7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
8 | 7 | raleqdv 3337 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2 ↔ ∀𝑒 ∈ ran (iEdg‘𝐺)(♯‘𝑒) = 2)) |
9 | | eqid 2738 |
. . . . . . 7
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
10 | | eqid 2738 |
. . . . . . 7
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
11 | 9, 10 | uspgrf 27269 |
. . . . . 6
⊢ (𝐺 ∈ USPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
12 | | f1f 6633 |
. . . . . . . . . 10
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
13 | 12 | frnd 6571 |
. . . . . . . . 9
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈
(𝒫 (Vtx‘𝐺)
∖ {∅}) ∣ (♯‘𝑥) ≤ 2}) |
14 | | ssel2 3909 |
. . . . . . . . . . . . . . 15
⊢ ((ran
(iEdg‘𝐺) ⊆
{𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2} ∧ 𝑦 ∈ ran (iEdg‘𝐺)) → 𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
15 | 14 | expcom 417 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ 𝑦 ∈ {𝑥 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2})) |
16 | | fveqeq2 6744 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑦 → ((♯‘𝑒) = 2 ↔ (♯‘𝑦) = 2)) |
17 | 16 | rspcv 3544 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (∀𝑒 ∈ ran (iEdg‘𝐺)(♯‘𝑒) = 2 →
(♯‘𝑦) =
2)) |
18 | | fveq2 6735 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (♯‘𝑥) = (♯‘𝑦)) |
19 | 18 | breq1d 5077 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) ≤ 2 ↔ (♯‘𝑦) ≤ 2)) |
20 | 19 | elrab 3614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) ≤ 2)) |
21 | | eldifi 4055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → 𝑦 ∈
𝒫 (Vtx‘𝐺)) |
22 | 21 | anim1i 618 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) = 2) → (𝑦 ∈ 𝒫 (Vtx‘𝐺) ∧ (♯‘𝑦) = 2)) |
23 | | fveqeq2 6744 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑦 → ((♯‘𝑥) = 2 ↔ (♯‘𝑦) = 2)) |
24 | 23 | elrab 3614 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2} ↔ (𝑦 ∈ 𝒫
(Vtx‘𝐺) ∧
(♯‘𝑦) =
2)) |
25 | 22, 24 | sylibr 237 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) = 2) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
26 | 25 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) → ((♯‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∧ (♯‘𝑦) ≤ 2) → ((♯‘𝑦) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
28 | 20, 27 | sylbi 220 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ((♯‘𝑦) =
2 → 𝑦 ∈ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2})) |
29 | 17, 28 | syl9 77 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (𝑦 ∈ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
30 | 15, 29 | syld 47 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ran (iEdg‘𝐺) → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
31 | 30 | com13 88 |
. . . . . . . . . . . 12
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}))) |
32 | 31 | imp 410 |
. . . . . . . . . . 11
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2})
→ (𝑦 ∈ ran
(iEdg‘𝐺) → 𝑦 ∈ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
33 | 32 | ssrdv 3921 |
. . . . . . . . . 10
⊢
((∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 ∧ ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2})
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2}) |
34 | 33 | ex 416 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (ran (iEdg‘𝐺) ⊆ {𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) =
2})) |
35 | 13, 34 | mpan9 510 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2) → ran (iEdg‘𝐺) ⊆ {𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
36 | | f1ssr 6640 |
. . . . . . . 8
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ran (iEdg‘𝐺)
⊆ {𝑥 ∈ 𝒫
(Vtx‘𝐺) ∣
(♯‘𝑥) = 2})
→ (iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
37 | 35, 36 | syldan 594 |
. . . . . . 7
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ ∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
38 | 37 | ex 416 |
. . . . . 6
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (∀𝑒 ∈
ran (iEdg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
39 | 11, 38 | syl 17 |
. . . . 5
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈ ran
(iEdg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
40 | 8, 39 | sylbid 243 |
. . . 4
⊢ (𝐺 ∈ USPGraph →
(∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2 → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
41 | 40 | imp 410 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2}) |
42 | 9, 10 | isusgrs 27271 |
. . . 4
⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
43 | 42 | adantr 484 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → (𝐺 ∈ USGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)–1-1→{𝑥 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑥) = 2})) |
44 | 41, 43 | mpbird 260 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2) → 𝐺 ∈ USGraph) |
45 | 5, 44 | impbii 212 |
1
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧
∀𝑒 ∈
(Edg‘𝐺)(♯‘𝑒) = 2)) |